proposition: Lemma prop_20 : forall A B C P Q, ~ Bet B A C -> SumS A B A C P Q -> Lt B C P Q.
proof: Proof. intros A B C P Q HNBet HSum. destruct (segment_construction B A A C) as [D [HBet HCong]]. apply (cong2_lt__lt B C B D); Cong. apply triangle_strict_inequality with A; Cong. apply (sums2__cong56 A B A C); trivial. exists B, A, D; repeat split; Cong. Qed.
imports: GeoCoq.Meta_theory.Continuity.elementary_continuity_props GeoCoq.Tarski_dev.Ch16_coordinates_with_functions