proposition: Lemma square_eq_weak : forall x a : F, x[^]2 [=] a[^]2 -> Not (x [#] a and x [#] [--]a).
proof: Proof. intros x a H. intro H0. elim H0; intros H1 H2. generalize (square_eq_aux _ _ H); intro H3. generalize (eq_imp_not_ap _ _ _ H3); intro H4. apply H4. apply mult_resp_ap_zero. astepr ([--]a[+]a). apply op_rht_resp_ap. auto. astepr (a[-]a). apply minus_resp_ap_rht. assumption. Qed.
imports: CoRN.algebra.CRings