proposition: Lemma t22_23_aux : forall A B C M N L, ~ Col A M N -> Per B C A -> A <> C -> Midpoint M A B -> Per M N A -> Col A C N -> Midpoint M N L -> Bet A N C /\ Lambert N L B C /\ Cong B L A N.
proof: Proof. intros A B C M N L HNCol HPerC HAC HM HPerN HColN HN. assert_diffs. assert (HBet : Bet A N C) by (apply per23_preserves_bet with M B; Perp; Col; Between). destruct (l11_49 A M N B M L) as [HCong1 [HCongA1 HCongA2]]; auto with cong. apply l11_14; Between. assert(B <> L) by (intro; treat_equalities; auto). repeat split; Cong. - intro; treat_equalities; apply HNCol; ColR. - intro; treat_equalities; apply H6. apply (l6_21 A M N M); Col. apply col_permutation_3, cop_per2__col with A; Col; Cop. - apply per_col with A; Col. apply l8_2, per_col with M; Col; Perp. - apply l8_2, per_col with A; Col. - apply l11_17 with M N A; auto. apply (l11_10 M N A M L B); auto; try (apply out_trivial; auto). apply l6_6, bet_out; Between. - apply coplanar_perm_16, col_cop__cop with M; Col. apply coplanar_perm_12, col_cop__cop with A; Col; Cop. Qed.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Tarski_dev.Annexes.saccheri GeoCoq.Tarski_dev.Ch13_1 GeoCoq.Meta_theory.Continuity.grad