proposition: Lemma prop_29_3 : forall A C G H P Q R, OS G H A C -> Par A G H C -> SumA A G H G H C P Q R -> Bet P Q R.
proof: Proof. intros A C G H P Q R HOS HPar. apply (suma_suppa__bet). apply alternate_interior__consecutive_interior; trivial. unfold alternate_interior_angles_postulate. apply l12_21_a. Qed.
imports: GeoCoq.Meta_theory.Continuity.elementary_continuity_props GeoCoq.Tarski_dev.Ch16_coordinates_with_functions