proposition: Lemma conga_to_par_os : forall A B C D P , Bet A D P -> OS A D B C -> CongA B A P C D P -> Par A B C D.
proof: Proof. intros A B C D P HBet HOS HCongA. assert_diffs. apply par_right_comm, l12_22_b with P; trivial. apply l6_6, bet_out; Between. apply invert_one_side, col_one_side with D; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec GeoCoq.Tarski_dev.Annexes.Tagged_predicates