proposition: Lemma compatibility_of_prod_with_order : forall O E E' A B AB, LeP O E E' O A -> LeP O E E' O B -> Prod O E E' A B AB -> LeP O E E' O AB.
proof: Proof. intros O E E' A B AB HLeA HLeB HAB. elim HLeA; clear HLeA; intro HLeA; elim HLeB; clear HLeB; intro HLeB; treat_equalities; try (apply prod_O_l_eq in HAB); try (apply prod_O_r_eq in HAB); treat_equalities; try (apply leP_refl). 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 (HColAB : Col O E AB) by (unfold Prod, Ar2 in *; spliter; Col). left; exists AB; split; try (apply diff_A_O); Col. destruct HLeA as [A' [HDiff1 HPsA]]; destruct HLeB as [B' [HDiff2 HPsB]]. assert (A = A') by (apply diff_uniqueness with O E E' A O; auto; apply diff_A_O; Col). assert (B = B') by (apply diff_uniqueness with O E E' B O; auto; apply diff_A_O; Col). treat_equalities; apply prod_pos_pos with E' A B; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch14_prod