proposition: Lemma prod_pos__signeq : forall O E E' A B C, A <> O -> B <> O -> Prod O E E' A B C -> Ps 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. contradiction. induction HB; auto. contradiction. induction H8; induction H9. { unfold SignEq. left. split; auto. } { apply pos_neg__prod_neg in H1; auto. apply pos_not_neg in H2. contradiction. } { apply prod_comm in H1. apply pos_neg__prod_neg in H1; auto. apply pos_not_neg in H2. contradiction. } { unfold SignEq. right. split; auto. } Qed.
imports: GeoCoq.Tarski_dev.Ch14_order