proposition: Lemma pos_inv_pos : forall O E E' A IA, O <> A -> LeP O E E' O A -> Prod O E E' IA A E -> LeP O E E' O IA.
proof: Proof. intros O E E' A IA HOA HLe HIA. elim HLe; clear HLe; intro HLe; treat_equalities; [|intuition]. 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 (HColIA : Col O E IA) by (unfold Prod, Ar2 in *; spliter; Col). destruct (diff_exists O E E' IA O) as [IA' HIA']; Col. assert (IA = IA') by (apply diff_uniqueness with O E E' IA O; auto; apply diff_A_O; Col). treat_equalities; left; exists IA; split; auto; clear HIA'. destruct HLe as [A' [HDiff HPs1]]. assert (A = A') by (apply diff_uniqueness with O E E' A O; auto; apply diff_A_O; Col). treat_equalities; clear HDiff; destruct (opp_exists O E E' HNC IA) as [MIA HMIA]; Col. assert (HElim := HMIA); apply pos_null_neg in HElim. elim HElim; clear HElim; intro HElim; auto. elim HElim; clear HElim; intro HPs2; treat_equalities. { assert (O = E) by (apply prod_uniqueness with O E E' O A; auto; apply prod_0_l; Col). treat_equalities; intuition. } { destruct (opp_exists O E E' HNC E) as [ME HME]; Col. assert (HColME : Col O E ME) by (unfold Opp, Sum, Ar2 in *; spliter; Col). assert (HProd1 : Prod O E E' IA ME MIA) by (apply opp_prod; auto). assert (HProd2 : Prod O E E' MIA A ME). { apply prod_assoc1 with ME IA E; auto; apply prod_comm; auto; apply prod_1_l; Col. } assert (HFalse : Ps O E ME) by (apply prod_pos_pos with E' MIA A; auto). apply opp_pos_neg with O E E' ME E in HFalse; try apply opp_comm; auto. exfalso; apply neg_not_pos in HFalse; apply HFalse. assert_diffs; repeat (split; Between). } Qed.
imports: GeoCoq.Tarski_dev.Ch14_prod