proposition: Lemma sac__cong : forall A B C D, Saccheri A B C D -> Cong A C B D.
proof: Proof. intros A B C D HSac. assert(Hdiff := sac_distincts A B C D HSac). unfold Saccheri in HSac. spliter. assert(HSAS := l11_49 B A D C D A). destruct HSAS; Cong; CongA. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma