proposition: Lemma ex_lambert : exists A B C D, Lambert A B C D.
proof: Proof. destruct ex_saccheri as [D [C [C' [D' HSac]]]]. destruct (midpoint_existence D D') as [A HA]. destruct (midpoint_existence C C') as [B HB]. exists A, B, C, D. apply mid2_sac__lam6521 with C' D'; trivial. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma