proposition: Lemma sac__conga : forall A B C D, Saccheri A B C D -> CongA A B C B C D.
proof: Proof. intros A B C D HSac. assert(Hdiff := sac_distincts A B C D HSac). assert(HCong := sac__cong A B C D HSac). unfold Saccheri in HSac. spliter. assert(HSSS := l11_51 A B C D C B). destruct HSSS as [_ []]; Cong; CongA. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma