proposition: Lemma t22_11__per : forall A B C D, Saccheri A B C D -> (CongA A B D B D C <-> Per A B C).
proof: Proof. intros A B C D HSac. split. - intro. apply (cong_sac__per _ _ _ D); auto. unfold Saccheri in HSac. spliter. assert(HSAS := l11_49 A B D C D B). destruct HSAS; Cong; CongA. - intro HPer. apply <- (cong_sac__per A B C D) in HPer; trivial. assert(Hdiff := sac_distincts A B C D HSac). unfold Saccheri in HSac. spliter. assert(HSSS := l11_51 A B D C D B). destruct HSSS as [_ []]; Cong; CongA. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma