proposition: Lemma cong2_sac2__cong : forall A B C D A' B' C' D', Saccheri A B C D -> Saccheri A' B' C' D' -> Cong A B A' B' -> Cong A D A' D' -> Cong B C B' C'.
proof: Proof. intros A B C D A' B' C' D' HSac HSac' HCongB HCongL. assert(Hdiff := sac_distincts A B C D HSac). assert(Hdiff' := sac_distincts A' B' C' D' HSac'). unfold Saccheri in *. spliter. destruct (l11_49 B A D B' A' D') as [HCongD [HConga1 HConga2]]; Cong; CongA. destruct (l11_49 B D C B' D' C'); Cong; [|apply (cong_transitivity _ _ A B); Cong; apply (cong_transitivity _ _ A' B'); Cong]. apply (l11_22b _ _ _ A _ _ _ A'). repeat (split; CongA); Side. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma