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