proposition: Lemma conga_per2_os__cong : forall A B C D, Per B A D -> Per A D C -> OS A D B C -> CongA B C D A B C -> Cong A B C D.
proof: Proof. intros A B C D HPer1 HPer2 Hos HCongA. destruct (or_lt_cong_gt A B C D) as [Hlt | [Hlt | Hcong]]; trivial; exfalso. - destruct (lt_os_per2__lta A B C D); auto. - unfold Gt in Hlt. apply lt_comm in Hlt. destruct (lt4321_os_per2__lta A B C D); CongA. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma