proposition: Lemma cong_sac__per : forall A B C D, Saccheri A B C D -> Cong A D B C <-> Per A B C.
proof: Proof. intros A B C D HSac. assert(HM := midpoint_existence B C). destruct HM as [M HM]. assert(HN := midpoint_existence A D). destruct HN as [N HN]. assert(HLam := mid2_sac__lam6521 A B C D M N HSac HM HN). apply sac_distincts in HSac; spliter. assert_diffs. split. - intro HCong. apply (per_col _ _ M); Col. apply l8_2, (cong_lam__per N); auto. apply cong_commutativity; apply (cong_cong_half_1 _ _ D _ _ C); auto. - intro HPer. apply cong_mid2__cong with N M; trivial. apply cong_commutativity, lam_per__cong; trivial. apply l8_2, per_col with C; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma