proposition: Lemma diff_2_le_le : forall O E E' A B C AMC BMC, Diff O E E' A C AMC -> Diff O E E' B C BMC -> LeP O E E' A B -> LeP O E E' AMC BMC.
proof: Proof. intros O E E' A B C AMC BMC HAMC HBMC HLe. assert (HNC : ~ Col O E E') by (apply diff_ar2 in HAMC; unfold Ar2 in *; spliter; Col). assert (HColC : Col O E C) by (apply diff_ar2 in HAMC; unfold Ar2 in *; spliter; Col). assert (HColAMC : Col O E AMC) by (apply diff_ar2 in HAMC; unfold Ar2 in *; spliter; Col). assert (HColBMC : Col O E BMC) by (apply diff_ar2 in HBMC; unfold Ar2 in *; spliter; Col). destruct (opp_exists O E E' HNC C) as [MC HMC]; Col. assert (HAMC' : Sum O E E' A MC AMC). { apply diff_sum in HAMC; apply sum_assoc_1 with AMC C O; apply sum_comm; auto; apply sum_O_B; Col. } assert (HBMC' : Sum O E E' B MC BMC). { apply diff_sum in HBMC; apply sum_assoc_1 with BMC C O; apply sum_comm; auto; apply sum_O_B; Col. } apply compatibility_of_sum_with_order with A B MC; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch14_prod