proposition: Lemma t22_24_aux1 : forall A B0 C0 E, ~ Col A B0 C0 -> Perp A C0 B0 C0 -> GradExp B0 C0 E -> exists B C, GradExp2 A B0 B B0 C0 E /\ Perp A C0 B C /\ Col A C0 C.
proof: Proof. intros A B0 C0 E HNCol HPerp0 HGE. induction HGE; rename A0 into B0; rename B into C0. exists B0; exists C0; repeat (split; Col); apply gradexp2_init. rename C into E; rename C' into E'. destruct IHHGE as [B [C [HGE2 [HPerp HCol]]]]; trivial. destruct (segment_construction A B A B) as [B' [HBet HCong]]. exists B'. destruct (l8_18_existence A C0 B') as [C' [HCol' HPerp']]. apply gradexp2__gradexp123, gradexp__grad, grad__bet in HGE2; intro; assert_diffs; apply HNCol; ColR. exists C'; repeat (split; trivial); apply gradexp2_stab with B E; Cong. Qed.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Tarski_dev.Annexes.saccheri GeoCoq.Tarski_dev.Ch13_1 GeoCoq.Meta_theory.Continuity.grad