proposition: Lemma t22_18_aux1 : forall A0 A1 E0 E1 D1 D, Bet A0 D1 A1 -> Cong E0 E1 A1 D1 -> Grad A0 D1 D -> exists A E, Grad2 A0 A1 A E0 E1 E /\ Cong E0 E A D /\ Bet A0 D A.
proof: Proof. intros A0 A1 E0 E1 D1 D HBet HCong HG. induction HG. exists A1; exists E1; repeat split; auto; apply grad2_init. rename A into A0. rename B into C1. destruct IHHG as [A [E [HG2 [HCong2 HBet2]]]]; auto. destruct (segment_construction A0 A A0 A1) as [A' [HBet3 HCong3]]. destruct (segment_construction E0 E E0 E1) as [E' [HBet4 HCong4]]. exists A'; exists E'. assert(HBet5 : Bet A0 C' A'). { assert(HBet5 : Bet A0 C A') by eBetween. assert(Bet C C' A'); [|eBetween]. apply grad2__grad123 in HG2. apply grad__bet in HG. apply grad__bet in HG2. elim(eq_dec_points A0 C). intro; treat_equalities; Between. intro. elim(eq_dec_points C C'). intro; treat_equalities; Between. intro. elim(eq_dec_points A' C). intro; subst A'; assert (A=C) by (apply (between_equality _ _ A0); Between); treat_equalities; Between. intro. apply l6_13_1. destruct (l6_2 C' A' A0 C); Between. apply (le_transitivity _ _ A A'). apply (l5_6 A0 C1 A0 A1); Cong; exists C1; split; Cong. destruct(l5_12_a C A A'); eBetween. } repeat split; auto. apply grad2_stab with A E; Cong. assert (HD : Le E0 E1 A A'). apply (l5_6 E0 E1 A1 A0); Cong; exists C1; split; Between. destruct HD as [D [HBet6 HCong6]]. apply (cong_transitivity _ _ C D). apply (l2_11 _ E _ _ A); Cong; eBetween; apply cong_transitivity with E0 E1; trivial. assert (Bet C D A') by eBetween. apply (l4_3 _ _ A' _ _ C); Cong; eBetween. apply (cong_transitivity _ _ A0 C1); Cong. apply cong_left_commutativity; apply (l4_3 _ _ A _ _ A1); Between; Cong. apply cong_transitivity with E0 E1; Cong. Qed.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Tarski_dev.Annexes.saccheri GeoCoq.Tarski_dev.Ch13_1 GeoCoq.Meta_theory.Continuity.grad