proposition: Lemma lam6534_mid2__sac : forall A B C D M N, Lambert N M C D -> 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. apply sac_perm. apply (lam6521_mid2__sac _ _ _ _ M N); Midpoint. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma