Propriétés de out_line

Definition out

out := fun P A B => A<>P /\ B<>P /\ (Bet P A B \/ Bet P B A)

Definition Inter

Inter := fun X P Q R S =>
      P <> Q /\ R <> S /\ Col X P Q /\ Col X R S /\
      ((exists Y, Col Y P Q /\ ~ Col Y R S) \/ (exists Y, ~ Col Y P Q /\ Col Y R S))

l6_2

forall A B C P, A<>P → B<>P → C<>P → Bet A P C → (Bet B P C ↔ out P A B)

l6_3_1

forall A B P, out P A B → (A <> P /\ B <> P /\ exists C, C <> P /\ Bet A P C /\ Bet B P C)

l6_3_2 (réciproque)

forall A B P, (A <> P /\ B <> P /\ exists C, C <> P /\ Bet A P C /\ Bet B P C) → out P A B

l6_4_1

forall A B P, out P A B → Col A P B /\ ~ Bet A P B

l6_4_2 (réciproque)

forall A B P, Col A P B /\ ~ Bet A P B → out P A B

l6_5 (out reflexivity)

forall P A, A <> P → out P A A

l6_6 (out symmetry)

forall P A B, out P A B → out P B A

l6_7 (out transitivity)

forall P A B C, out P A B → out P B C → out P A C

l6_11_unicity

forall A B C R X Y,
R <> A → B <> C → out A X R → Cong A X B C → out A Y R → Cong A Y B C → X=Y

l6_11_existence

forall A B C R, R <> A → B <> C → exists X, out A X R /\ Cong A X B C

l6_13_1

forall P A B, out P A B → le P A P B → Bet P A B

l6_13_2

forall P A B, out P A B → Bet P A B → le P A P B

l6_16_1

forall P Q S X, P <> Q → S <> P → Col S P Q → (Col X P Q → Col X P S)

l6_16_2

forall P Q S X, P <> Q → S <> P → Col S P Q → (Col X P S -> Col X P Q)

col_transitivity_1

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

col_transitivity_2

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

l6_21

forall A B C D P Q,
~ Col A B C → C <> D -> Col A B P → Col A B Q → Col C D P → Col C D Q → P = Q

l6_25

forall A B, A<>B → exists C, ~ Col A B C

t2_8

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