Propriétés de congruence des angles

Definition Conga

Conga := fun A B C D E F =>
A ≠ B /\ C ≠ B /\ D ≠ E /\ F ≠ E /\
exists A', exists C', exists D', exists F',
Bet B A A' /\ Cong A A' E D /\
Bet B C C' /\ Cong C C' E F /\
Bet E D D' /\ Cong D D' B A /\
Bet E F F' /\ Cong F F' B C /\
Cong A' C' D' F'

l11_aux

forall B A A' A0 E D D' D0,
out B A A' → out E D D' → Cong B A' E D'
→ Bet B A A0 → Bet E D D0 → Cong A A0 E D → Cong D D0 B A
→ Cong B A0 E D0 /\ Cong A' A0 D' D0

l11_3

forall A B C D E F,
Conga A B C D E F → exists A', exists C', exists D', exists F',
       out B A' A /\ out B C C' /\ out E D' D /\ out E F F' /\ Cong_3 A' B C' D' E F'

l11_3_bis

forall A B C D E F,
(exists A', exists C', exists D', exists F',
      out B A' A /\ out B C' C /\ out E D' D /\ out E F' F /\ Cong_3 A' B C' D' E F')
          → Conga A B C D E F

l11_4_1

forall A B C D E F,
Conga A B C D E F → A≠B /\ C≠B /\ D≠E /\ F≠E /\
      (forall A' C' D' F', out B A' A /\ out B C' C /\ out E D' D /\ out E F' F /\
            Cong B A' E D' /\ Cong B C' E F' → Cong A' C' D' F')

l11_4_2

forall A B C D E F,
(A ≠ B /\ C ≠ B /\ D ≠ E /\ F ≠ E /\
      (forall A' C' D' F', out B A' A /\ out B C' C /\ out E D' D /\ out E F' F /\
            Cong B A' E D' /\ Cong B C' E F' → Cong A' C' D' F')) → Conga A B C D E F

conga_refl

forall A B C, A ≠ B → C ≠ B → Conga A B C A B C

conga_sym

forall A B C A' B' C', Conga A B C A' B' C' → Conga A' B' C' A B C

conga_trans

forall A B C A' B' C' A'' B'' C'',
Conga A B C A' B' C' → Conga A' B' C' A'' B'' C'' → Conga A B C A'' B'' C''

conga_pseudo_refl

forall A B C, A ≠ B → C ≠ B → Conga A B C C B A

conga_trivial1

forall A B C D, A ≠ B → C ≠ D → Conga A B A C D C

conga_trivial2

forall A B, Conga A A A B B B

l11_10

forall A B C D E F A' C' D' F',
Conga A B C D E F → out B A' A → out B C' C → out E D' D → out E F' F → Conga A' B C' D' E F'

l11_13

forall A B C D E F A' D',
Conga A B C D E F → Bet A B A' → A'<> B → Bet D E D' → D'<> E → Conga A' B C D' E F

conga_left_comm

forall A B C D E F, Conga A B C D E F → Conga C B A D E F

conga_right_comm

forall A B C D E F, Conga A B C D E F → Conga A B C F E D

conga_comm

forall A B C D E F, Conga A B C D E F → Conga C B A F E D

Definition Distincts

Distincts := fun A B C => A ≠ B /\ A ≠ C /\ B ≠ C

conga_line

forall A B C A' B' C', Distincts A B C → Distincts A' B' C' → Bet A B C → Bet A' B' C'
→ Conga A B C A' B' C'

l11_14

forall A B C A' C', Bet A B A' → Distincts A B A' → Bet C B C' → Distincts C B C'
→ Conga A B C A' B C'

l11_16

forall A B C A' B' C', Per A B C → A ≠ B → C ≠ B → Per A' B' C' → A' ≠ B' → C' ≠ B'
→ Conga A B C A' B' C'

l11_17

forall A B C A' B' C', Per A B C → Conga A B C A' B' C' → Per A' B' C'

l11_18_a

forall A B C D, Bet C B D → Distincts B C D → A<>B → Per A B C → Conga A B C A B D

l11_18_b

forall A B C D, Bet C B D → Distincts B C D → A<>B → Conga A B C A B D → Per A B C

l11_19

forall A B P1 P2, Per A B P1 → Per A B P2 → one_side A B P1 P2 → out B P1 P2

l11_21_a (null angle)

forall A B C A' B' C', out B A C → Conga A B C A' B' C' → out B' A' C'

l11_21_b (null angle)

forall A B C A' B' C', out B A C → out B' A' C' → Conga A B C A' B' C'

l11_22_aux

forall A B C C', Conga A B C A B C' → out B C C' \/ two_sides A B C C'