proposition: Lemma le_pos_prod_le : forall O E E' A B C AC BC, LeP O E E' A B -> LeP O E E' O C -> Prod O E E' A C AC -> Prod O E E' B C BC -> LeP O E E' AC BC.
proof: Proof. intros O E E' A B C AC BC HALeB HPsC HAC HBC. assert (HNC : ~ Col O E E') by (unfold Prod, Ar2 in *; spliter; Col). assert (HColA : Col O E A) by (unfold Prod, Ar2 in *; spliter; Col). assert (HColB : Col O E B) by (unfold Prod, Ar2 in *; spliter; Col). assert (HColC : Col O E C) by (unfold Prod, Ar2 in *; spliter; Col). assert (HColAC : Col O E AC) by (unfold Prod, Ar2 in *; spliter; Col). assert (HColBC : Col O E BC) by (unfold Prod, Ar2 in *; spliter; Col). destruct (diff_exists O E E' BC AC) as [BCMAC HBCMAC]; Col. apply compatibility_of_sum_with_order with O BCMAC AC; try apply sum_O_B; try (apply sum_comm; try apply diff_sum); Col. destruct (diff_exists O E E' B A) as [BMA HBMA]; Col. assert (HColBMA : Col O E BMA) by (apply diff_ar2 in HBMA; unfold Ar2 in *; spliter; Col). destruct (prod_exists O E E' HNC BMA C) as [BCMAC' HBCMAC']; Col. assert (H : Diff O E E' BC AC BCMAC'). { apply sum_diff; apply diff_sum in HBMA; apply distr_r with A BMA C B; auto. } assert (BCMAC = BCMAC') by (apply diff_uniqueness with O E E' BC AC; auto). clear H; treat_equalities; apply compatibility_of_prod_with_order with BMA C; auto. destruct (opp_exists O E E' HNC A) as [MA HMA]; Col. assert (HColMA : Col O E MA) by (unfold Opp, Sum, Ar2 in *; spliter; Col). apply compatibility_of_sum_with_order with A B MA; auto; try (apply diff_sum; apply diff_O_A; Col). apply diff_O_A in HMA; Col; apply diff_sum in HBMA; apply diff_sum in HMA. apply sum_assoc_1 with BMA A O; auto; try apply sum_A_O; Col. apply sum_comm; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch14_prod