proposition: Lemma t22_18_aux2 : forall A0 A1 B0 B1 A B E, Saccheri A0 B0 B1 A1 -> Grad2 A0 A1 A B0 B1 E -> Saccheri A0 B0 B A -> Le B0 B B0 E.
proof: Proof. intros A0 A1 B0 B1 A B E HSac1 HG. revert B. induction HG; rename A into A0; rename B into A1; rename D into B0; rename E into B1. { intros B HSac. assert(B = B1); [|subst B; Le]. assert(Hdiff := sac_distincts A0 B0 B1 A1 HSac1); unfold Saccheri in *; spliter. apply (l6_11_uniqueness A1 A0 B0 B1); Cong; [|apply out_trivial; auto]. apply (col_one_side_out _ A0). apply col_permutation_2, cop_per2__col with A0; Perp. apply coplanar_perm_3, coplanar_trans_1 with B0; Cop. apply not_col_permutation_2, one_side_not_col123 with B1; assumption. apply (one_side_transitivity _ _ _ B0); Side. } rename C into A; rename F into E; rename C' into A'; rename F' into E'. intros B' HSac'. assert (A0 <> A). { intro; treat_equalities. assert (A0 = A1) by (apply between_identity, grad__bet, (grad2__grad123 _ _ _ B0 B1 E); auto). treat_equalities. apply sac_distincts in HSac1; spliter; auto. } assert (HB : exists B, Saccheri A0 B0 B A). { clear dependent A'; clear dependent B'; clear IHHG. apply grad2__grad123 in HG. apply grad__bet in HG. destruct (l10_15 A0 A1 A B0) as [P [HPerp HOS]]; Col. apply par_strict_not_col_1 with B1, sac__pars1423, HSac1. destruct (l6_11_existence A A0 B0 P) as [B [HOut Hcong5]]. assert_diffs; auto. assert(Hdiff := sac_distincts A0 B0 B1 A1 HSac1); spliter; auto. exists B. unfold Saccheri in *; spliter; assert_diffs. repeat split; Cong. - apply (per_col _ _ A1); Col. - apply perp_per_2, (perp_col1 _ _ _ P); Col. apply perp_comm; apply (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. } destruct HB as [B HSac]. assert (HLe := HSac). apply IHHG in HLe; auto. clear IHHG. destruct (segment_construction B0 B E E') as [C [HBet HCong]]. assert (Cong B0 B1 B B'). apply (cong2_sac2__cong A0 B0 B1 A1 A _ _ A'); auto; [|unfold Saccheri in *; spliter; Cong]. apply cop_sac2__sac with A0 B0; Cop. intro; treat_equalities; apply sac_distincts in HSac1; spliter; auto. apply (le_transitivity _ _ B0 C). apply (triangle_inequality B0 B B' C); trivial. apply cong_transitivity with E E'; Cong. apply cong_transitivity with B0 B1; Cong. apply (bet2_le2__le1346 _ B _ _ E); Le. Qed.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Tarski_dev.Annexes.saccheri GeoCoq.Tarski_dev.Ch13_1 GeoCoq.Meta_theory.Continuity.grad