proposition: Lemma prop_21_2 : forall A B C D A1 A2 D1 D2, OS A B C D -> OS B C A D -> OS A C B D -> SumS A B A C A1 A2 -> SumS D B D C D1 D2 -> Lt D1 D2 A1 A2.
proof: Proof. intros A B C D A1 A2 D1 D2; intros. assert (HNCol : ~ Col A B C) by (apply one_side_not_col123 with D; assumption). destruct (os2__inangle A B C D) as [HAB [HCB [HDB [E [HBet [Heq|HOut]]]]]]; Side. subst; exfalso; apply HNCol; ColR. assert_diffs. assert (A <> E) by (intro; subst E; apply (one_side_not_col124 A B C D); Col). assert (C <> E) by (intro; subst E; apply (one_side_not_col124 B C A D); Col). assert (D <> E) by (intro; subst E; apply (one_side_not_col124 A C B D); Col). assert (Bet B D E). apply out2__bet; [apply l6_6, HOut|]. apply col_one_side_out with A; Col. apply invert_one_side, col_one_side with C; Col. destruct (ex_sums E B E C) as [P [Q]]. apply lt_transitivity with P Q. - destruct (ex_sums E C E D) as [R [S]]. apply le_lt34_sums2__lt with D B D C D B R S; Le. apply prop_20 with E; Sums. intro; apply HNCol; ColR. apply sums_assoc_1 with E D E C E B; Sums. - destruct (ex_sums A B A E) as [R [S]]. apply le_lt12_sums2__lt with E B E C R S E C; Le. apply prop_20 with A; Sums. intro; apply HNCol; ColR. apply sums_assoc_2 with A B A E A C; Sums. Qed.
imports: GeoCoq.Meta_theory.Continuity.elementary_continuity_props GeoCoq.Tarski_dev.Ch16_coordinates_with_functions