proposition: Lemma prop_32_1 : forall A B C D E F, TriSumA A B C D E F -> Bet D E F.
proof: Proof. apply alternate_interior__triangle. 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