Propriétés de la congruence

cong_reflexivity

forall A B : Point, Cong A B A B

cong_symmetry

forall A B C D : Point, Cong A B C D → Cong C D A B

cong_transitivity

forall A B C D E F : Point, Cong A B C D → Cong C D E F → Cong A B E F

cong_left_commutativity

forall A B C D, Cong A B C D → Cong B A C D.

cong_right_commutativity

forall A B C D, Cong A B C D → Cong A B D C

cong_commutativity

forall A B C D, Cong A B C D → Cong B A D C

cong_trivial_identity

forall A B : Point, Cong A A B B

cong_reverse_identity

forall A C D, Cong A A C D → C=D

Définition : OFSC

OFSC := fun A B C D A' B' C' D' =>
Bet A B C /\ Bet A' B' C' /\
Cong A B A' B' /\ Cong B C B' C' /\
Cong A D A' D' /\ Cong B D B' D'.

(voir IFSC - FSC)

five_segments_with_def

forall A B C D A' B' C' D',
OFSC A B C D A' B' C' D' → A<>B → Cong C D C' D'

(voir l4_2 - l4_16)

l2_11

forall A B C A' B' C',
Bet A B C → Bet A' B' C' →
Cong A B A' B' → Cong B C B' C' → Cong A C A' C'

(voir l4_3)

construction_unicity

forall Q A B C x y,
Q ≠ A → Bet Q A x → Cong A x B C → Bet Q A y → Cong A y B C → x=y.