proposition: Lemma cong_lam__per : forall A B C D, Lambert A B C D -> Cong A D B C -> Per B C D.
proof: Proof. intros A B C D HLam HCong. assert (HLam' := HLam). unfold Lambert in HLam'. spliter. apply l8_2, (l11_17 A D C); auto. apply sac__conga. repeat split; Perp; Cong. apply one_side_symmetry, l12_6, lam__pars1234, HLam. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma