proposition: Lemma opp_2_le_le : forall O E E' A MA B MB, Opp O E E' A MA -> Opp O E E' B MB -> LeP O E E' A B -> LeP O E E' MB MA.
proof: Proof. intros O E E' A MA B MB HOppA HOppB HLe. assert (HNC : ~ Col O E E') by (unfold Opp, Sum, Ar2 in *; spliter; Col). assert (HColA : Col O E A) by (unfold Opp, Sum, Ar2 in *; spliter; Col). assert (HColMA : Col O E MA) by (unfold Opp, Sum, Ar2 in *; spliter; Col). assert (HColB : Col O E B) by (unfold Opp, Sum, Ar2 in *; spliter; Col). assert (HColMB : Col O E MB) by (unfold Opp, Sum, Ar2 in *; spliter; Col). destruct (sum_exists O E E' HNC MA MB) as [MAMB HMAMB]; Col. assert (HMA : Sum O E E' B MAMB MA) by (apply sum_assoc_2 with MB MA O; apply sum_comm; Col; apply sum_A_O; auto). assert (HMB : Sum O E E' A MAMB MB) by (apply sum_assoc_2 with MA MB O; try apply sum_O_B; auto; apply sum_comm; auto). eapply compatibility_of_sum_with_order in HLe; [|apply HMB|apply HMA]; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch14_prod