proposition: Lemma lt_os_per2__lta : forall A B C D, Per B A D -> Per A D C -> OS A D B C -> Lt A B C D -> LtA B C D A B C.
proof: Proof. intros A B C D HPer1 HPer2 Hos Hlt. apply lt_right_comm in Hlt. destruct Hlt as [[E []] HNCong]. assert(E<>C) by (intro; subst; auto). assert(~ Col A D B) by (apply (one_side_not_col123 _ _ _ C); auto). assert(~ Col A D C) by (apply (one_side_not_col123 _ _ _ B); Side). assert_diffs. assert(HNCol1 := per2_os__ncol123 A B C D HPer1 HPer2 Hos). assert(HNCol2 := per2_os__ncol234 A B C D HPer1 HPer2 Hos). assert(HSac : Saccheri A B E D). { repeat split; Cong. apply (per_col _ _ C); Col. apply (one_side_transitivity _ _ _ C); auto. apply one_side_symmetry; apply invert_one_side. apply out_one_side. right; Col. apply bet_out; auto. } assert(HNCol3 : ~ Col E C B) by (intro; apply HNCol2; ColR). assert(Par_strict A B C D). { apply (par_not_col_strict _ _ _ _ D); Col. apply (l12_9 _ _ _ _ A D); Perp; Cop. } assert_diffs. apply (lta_trans _ _ _ B E D). - assert(HInter := l11_41 E C B D). destruct HInter; Between. apply (conga_preserves_lta E C B B E D); try (apply conga_refl); auto. apply (l11_10 E C B B C E); try (apply out_trivial); CongA. apply l6_6, bet_out; Between. - apply (conga_preserves_lta A B E A B C); try (apply conga_refl); auto. apply sac__conga; auto. split. { apply inangle__lea. apply os2__inangle. - apply l12_6. apply (par_strict_col_par_strict _ _ _ D); Par; Col. - apply (one_side_transitivity _ _ _ D); [|apply invert_one_side, one_side_symmetry, out_one_side; Out; Col]. destruct (par_one_or_two_sides A B D C) as [[]|[]]; Par. exfalso; apply (l9_9 A D B C); trivial. } intro. assert (Out B E C). apply (conga_os__out A); trivial; apply one_side_symmetry, par_strict_one_side with D; Col. apply HNCol3; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma