proposition: Lemma lam6521_mid2__sac : forall A B C D M N, Lambert N M B A -> Midpoint M B C -> Midpoint N A D -> Saccheri A B C D.
proof: Proof. intros A B C D M N HLam HM HN. assert (HLam' := HLam). unfold Lambert in HLam'. spliter. assert_diffs. assert(Per D A B) by (apply (l8_3 N); Col). assert(ReflectL D A M N). { split. exists N; Col. left; apply (perp_col1 _ _ _ N); Col; Perp. } assert(ReflectL A D M N) by (apply l10_4_spec; auto). assert(ReflectL C B M N). { split. exists M; Col. left; apply (perp_col1 _ _ _ M); Col; Perp. } assert(ReflectL B C M N) by (apply l10_4_spec; auto). repeat split; auto. - Perp. - apply (image_spec_preserves_per D A B _ _ _ M N); auto. - apply cong_left_commutativity. apply (l10_10_spec M N); auto. - apply (col_one_side _ N); Col. apply l12_6. apply (par_strict_col_par_strict _ _ _ M); Col. apply lam__pars1423 in HLam; Par. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma