Définition : Col

Col (A B C : Point) : Prop := Bet A B C \/ Bet B C A \/ Bet C A B

Permutations

col_permutation_1 : forall A B C, Col A B C → Col B C A

col_permutation_2 : forall A B C, Col A B C → Col C A B

col_permutation_3 : forall A B C, Col A B C → Col C B A

col_permutation_4 : forall A B C, Col A B C → Col B A C

col_permutation_5 : forall A B C, Col A B C → Col B A C

Trivial

col_trivial_1 : forall A B, Col A A B

col_trivial_2 : forall A B, Col A B B

col_trivial_3 : forall A B, Col A B A

l4_13

forall A B C A' B' C', Col A B C → Cong_3 A B C A' B' C' → Col A' B' C'

(voir l4_6)

l4_14

forall A B C A' B',
Col A B C → Cong A B A' B' → exists C', Cong_3 A B C A' B' C'

(voir l4_5)

Définition : FSC

FSC := fun A B C D A' B' C' D' =>
Col A B C /\ Cong_3 A B C A' B' C' /\ Cong A D A' D' /\ Cong B D B' D'

Sorry, the GeoGebra Applet could not be started. Please make sure that Java 1.4.2 (or later) is installed and active in your browser (Click here to install Java now)

(voir IFSC - OFSC)

l4_16

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

Sorry, the GeoGebra Applet could not be started. Please make sure that Java 1.4.2 (or later) is installed and active in your browser (Click here to install Java now)

(voir five_segments_with_def - l4_2)

l4_17

forall A B C P Q,
A<>B → Col A B C → Cong A P A Q → Cong B P B Q → Cong C P C Q

Sorry, the GeoGebra Applet could not be started. Please make sure that Java 1.4.2 (or later) is installed and active in your browser (Click here to install Java now)

l4_18

forall A B C C', A ≠ B -> Col A B C → Cong A C A C' → Cong B C B C' → C=C'

l4_19

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