proposition: Lemma euclid_22_aux : forall A B C D E F A' B' E' F' C1 C2 E1, SumS A B C D E' F' -> SumS C D E F A' B' -> Le E F E' F' -> Le A B A' B' -> Out A B C1 -> Cong A C1 C D -> Bet B A C2 -> Cong A C2 C D -> Out B A E1 -> Cong B E1 E F -> Bet C1 E1 C2.
proof: Proof. intros A B C D E F A' B' E' F'; intros. assert (Bet C1 A C2) by (assert_diffs; apply l6_2 with B; auto). apply not_out_bet. ColR. intro HOut; destruct HOut as [HC1E1 [HC2E1 [HBet|HBet]]]. - assert (Bet A C1 E1) by eBetween. assert (Bet A E1 B). apply out2__bet; trivial. apply l6_7 with C1; apply l6_6; trivial. assert_diffs; apply bet_out; trivial. apply (le__nlt A B A' B'); trivial. apply le_lt12_sums2__lt with C D E F A E1 E1 B; Sums; Le. split. exists C1; split; Cong. intro HCong. apply HC1E1, between_cong with A; trivial. apply cong_transitivity with C D; trivial. - assert (Bet A C2 E1) by eBetween. assert (Bet B C2 E1) by (assert_diffs; apply l6_2 with A; auto; apply bet_out; Between). apply (le__nlt E F E' F'); trivial. apply (cong2_lt__lt B C2 B E1); Cong. split; [exists C2; Cong|]. intro HCong. apply HC2E1, between_cong with B; trivial. apply (sums2__cong56 A B C D); trivial; exists B, A, C2; repeat split; Cong. Qed.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Tarski_dev.Annexes.circles GeoCoq.Tarski_dev.Annexes.sums GeoCoq.Utils.all_equiv