proposition: Lemma square_not_neg : forall O E E' A A2, Prod O E E' A A A2 -> ~Ng O E A2.
proof: Proof. intros. intro. assert(O <> E /\ Col O E A). { unfold Prod in H. unfold Ar2 in H. spliter. split; Col. intro; subst E; Col. } spliter. assert(HP:=signEq_refl O E A H1 H2). spliter. induction HP. { subst A. assert(HH:=prod_O_l_eq O E E' O A2 H). unfold Ng in H0. spliter. contradiction. } { assert(HH:= signeq__prod_pos O E E' A A A2 H3 H). apply pos_not_neg in HH. contradiction. } Qed.
imports: GeoCoq.Tarski_dev.Ch14_order