proposition: Lemma prop_28_2 : forall A C G H P Q R, OS G H A C -> SumA A G H G H C P Q R -> Bet P Q R -> Par A G C H.
proof: Proof. intros A C G H P Q R HOS HSumA HBet. destruct (segment_construction C H C H) as [D [HBet1 HCong]]. apply par_comm. assert_diffs. apply par_col_par with D; Col. apply l12_21_b. - apply l9_8_2 with C; Side. assert (HNCol := one_side_not_col124 G H A C HOS). repeat split; Col. intro; apply HNCol; ColR. exists H; Col. - apply suppa2__conga123 with G H C. apply bet_suma__suppa with P Q R; assumption. split; auto; exists C; split; [Between|CongA]. Qed.
imports: GeoCoq.Meta_theory.Continuity.elementary_continuity_props GeoCoq.Tarski_dev.Ch16_coordinates_with_functions