proposition: Lemma t22_18 : archimedes_axiom -> forall A0 B0 B1 A1, Saccheri A0 B0 B1 A1 -> ~ Lt B0 B1 A1 A0.
proof: Proof. intros Harchi A0 B0 B1 A1 HSac. intro Hlt. destruct Hlt as [Hle HNcong]. destruct Hle as [D1 [Hbet Hcong]]. destruct (segment_construction A0 D1 A0 B0) as [C0 [Hbet2 Hcong2]]. destruct (segment_construction A0 C0 A0 B0) as [C [Hbet3 Hcong3]]. assert(H : forall D, Grad A0 D1 D -> Lt A0 D A0 C). { intros D HG. destruct (t22_18_aux1 A0 A1 B0 B1 D1 D) as [A [E [HG2 [Hcong4 Hbet4]]]]; Between. assert (Hbet5 := grad2__grad123 A0 A1 A B0 B1 E HG2). apply grad__bet in Hbet5. destruct (l10_15 A0 A1 A B0) as [P [HPerp HOS]]. Col. apply par_strict_not_col_1 with B1, sac__pars1423, HSac. destruct (l6_11_existence A A0 B0 P) as [B [HOut Hcong5]]. assert_diffs; auto. assert(Hdiff := sac_distincts A0 B0 B1 A1 HSac); spliter; auto. assert(HSac2 : Saccheri A0 B0 B A). { unfold Saccheri in *; spliter; assert_diffs; assert(A0 <> A) by (intro; treat_equalities; auto). repeat split; Cong. - apply (per_col _ _ A1); Col. - apply perp_per_2, (perp_col1 _ _ _ P); Col. apply perp_comm, (perp_col _ A1); Col. - apply invert_one_side. apply (out_out_one_side _ _ _ P); [|apply l6_6; auto]. apply invert_one_side. apply (col_one_side _ A1); Col. } assert(HLe : Le B0 B B0 E) by (apply (t22_18_aux2 A0 A1 B0 B1 A); auto). assert (HLe2 : Le B0 B A A0). apply (le_transitivity _ _ B0 E); auto. apply (l5_6 A D A A0); Cong. destruct (l5_12_a A D A0); Between. assert (HLe2' := HLe2). destruct HLe2' as [Q [Hbet6 Hcong6]]. apply (le1234_lt__lt _ _ A0 Q). apply (bet2_le2__le1245 _ _ A _ _ A); Between; Le. apply (l5_6 B0 B B0 E); Cong. clear dependent D; clear dependent E. destruct (l6_11_existence A0 A0 B0 A) as [B0' [HOut2 Hcong4]]; try (assert_diffs; intro; treat_equalities; auto). destruct (segment_construction A0 B0' B0 B) as [B' [Hbet7 Hcong7]]. destruct (segment_construction B0' B' B A) as [A' [Hbet8 Hcong8]]. assert (Le A0 A A0 A'). { destruct (segment_construction A0 B0' B0 A) as [B'' [Hbet9 Hcong9]]. apply (le_transitivity _ _ A0 B''). apply (triangle_inequality_2 _ B0 _ _ B0'); Cong. apply (bet2_le2__le1346 _ B0' _ _ B0'); Le. apply (outer_transitivity_between _ _ B'); auto. intro; treat_equalities; apply sac_distincts in HSac2; spliter; auto. apply (l5_6 B0 A B0' A'); Cong. apply (triangle_inequality_2 _ B _ _ B'); Cong. } assert (HLe3 : Le B0 B A' B0'). apply (l5_6 B0' B' B0' A'); Cong; destruct (l5_12_a B0' B' A'); auto. destruct HLe3 as [Q' [Hbet9 Hcong9]]. assert (HBet10 : Bet A0 B0' A'). apply sac_distincts in HSac2; spliter; assert_diffs. apply (outer_transitivity_between _ _ B'); Between. apply (le1234_lt__lt _ _ A0 Q'). apply (bet2_le2__le1245 _ _ A' _ _ A); eBetween. apply cong__le; apply (cong_transitivity _ _ B0 B); Cong. assert (Cong B0' Q' A0 B0). { apply (cong_transitivity _ _ A B); Cong. apply (cong_transitivity _ _ A' B'); Cong. assert(Hcong10 : Cong B0' B' A' Q') by (apply (cong_transitivity _ _ B0 B); auto). elim(bet_dec B0' Q' B'). intro; apply (l4_3 _ _ B' _ _ Q'); Cong; eBetween. intro HNBet. apply sac_distincts in HSac2; spliter; assert_diffs. assert (Q' <> B0') by (intro; subst; apply HNBet; Between). assert (A' <> B0') by (intro; treat_equalities; auto). assert (HOut3 : Out B0' B' Q'). apply (l6_7 _ _ A'); [| apply l6_6]; apply bet_out; Between. assert (Hbet11 : Bet B0' B' Q'). apply out2__bet; auto. apply not_bet_out; Col. apply (l2_11 _ B' _ _ Q'); Cong; eBetween. } assert (Hbet10 : Bet A0 D1 C) by eBetween. apply (cong2_lt__lt D1 C A0 C); Cong; [split|]. destruct (l5_12_a A0 D1 C); auto. intro; assert (D1 = A0) by (apply (between_cong C); Between; Cong); treat_equalities; Cong. apply (l2_11 _ C0 _ _ B0'); eBetween; apply cong_transitivity with A0 B0; Cong. } unfold archimedes_axiom in *. specialize Harchi with A0 D1 A0 C. destruct Harchi as [D [HG Hle]]. intro; treat_equalities; auto. assert(HLt := HG). apply H in HLt. apply grad__le in HG. apply (le__nlt A0 C A0 D); auto. Qed.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Tarski_dev.Annexes.saccheri GeoCoq.Tarski_dev.Ch13_1 GeoCoq.Meta_theory.Continuity.grad