proposition: Lemma opp_prod : forall O E E' ME X MX, Opp O E E' E ME -> Opp O E E' X MX -> Prod O E E' X ME MX.
proof: Proof. intros O E E' ME X MX HOpp1 HOpp2. assert (HNC : ~ Col O E E') by (unfold Opp, Sum, Ar2 in *; spliter; Col). assert (HCol1 : Col O E ME) by (unfold Opp, Sum, Ar2 in *; spliter; Col). assert (HCol2 : Col O E X) by (unfold Opp, Sum, Ar2 in *; spliter; Col). destruct (sum_exists O E E' HNC E ME) as [EPME HEPME]; Col. assert (O = EPME) by (apply sum_uniqueness with O E E' E ME; auto; apply diff_sum; apply diff_O_A; Col). treat_equalities; destruct (prod_exists O E E' HNC X E) as [X' HX]; Col. assert (X = X') by (apply prod_uniqueness with O E E' X E; auto; apply prod_1_r; Col). treat_equalities; destruct (prod_exists O E E' HNC X O) as [O' HProd]; Col. assert (O = O') by (apply prod_uniqueness with O E E' X O; auto; apply prod_0_r; Col). treat_equalities; destruct (prod_exists O E E' HNC X ME) as [MX' HMX]; Col. assert (HOpp3 : Sum O E E' X MX' O) by (apply distr_l with X E ME O; auto). apply sum_opp in HOpp3; assert (MX = MX') by (apply opp_uniqueness with O E E' X; Col). treat_equalities; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch14_sum