proposition: Lemma not_signEq_prod_neg : forall O E E' A B C, A <> O -> B <> O -> ~SignEq O E A B -> Prod O E E' A B C -> Ng O E C.
proof: Proof. intros. assert(HP:=H2). unfold Prod in HP. unfold Ar2 in HP. spliter. clear H4. assert(O <> E). { intro; subst E; apply H1; Col. apply False_ind; Col. } assert(HA:=sign_dec O E A H5 H4). assert(HB:= sign_dec O E B H6 H4). induction HA; induction HB; try contradiction. induction H8;induction H9. { apply False_ind. apply H1. unfold SignEq. left; auto. } { apply(pos_neg__prod_neg O E E' A B); auto. } { apply prod_comm in H2. apply(pos_neg__prod_neg O E E' B A); auto. } { apply False_ind. apply H1. unfold SignEq. right; auto. } Qed.
imports: GeoCoq.Tarski_dev.Ch14_order