proposition: Lemma mid2_sac__lam6521 : forall A B C D M N, Saccheri A B C D -> Midpoint M B C -> Midpoint N A D -> Lambert N M B A.
proof: Proof. intros A B C D M N HSac HM HN. unfold Lambert. assert(Hdiff := sac_distincts A B C D HSac). assert(HPerp1 := mid2_sac__perp_lower A B C D M N HSac HM HN). assert(HPerp2 := mid2_sac__perp_upper A B C D M N HSac HM HN). unfold Saccheri in HSac. spliter. assert_diffs. repeat split; auto. - apply perp_per_1, (perp_col1 _ _ _ D); Perp; Col. - apply (l8_3 D); Perp; Col. - apply perp_per_1; auto. apply (perp_col1 _ _ _ C); Perp; Col. - apply coplanar_perm_5, col_cop__cop with C; Col. apply coplanar_perm_22, col_cop__cop with D; Col; Cop. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma