proposition: Lemma mid2_sac__lam6534 : forall A B C D M N, Saccheri A B C D -> Midpoint M B C -> Midpoint N A D -> Lambert N M C D.
proof: Proof. intros A B C D M N HSac HM HN. apply (mid2_sac__lam6521 _ _ B A); [apply sac_perm|apply l7_2..]; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma