proposition: Lemma cond_square_eq : forall x a : F, (Two:F) [#] [0] -> a [#] [0] -> x[^]2 [=] a[^]2 -> x [=] a or x [=] [--]a.
proof: Proof. intros x a H Ha H0. cut (a [#] [--]a). intro H1. elim (ap_cotransitive_unfolded _ _ _ H1 x); intro H2. right. apply not_ap_imp_eq. intro H3. elim (square_eq_weak _ _ H0). split; auto. apply ap_symmetric_unfolded; auto. left. apply not_ap_imp_eq. intro H3. elim (square_eq_weak _ _ H0); auto. apply plus_cancel_ap_lft with a. astepr ([0]:F). astepl (Two[*]a). apply mult_resp_ap_zero; auto. Qed.
imports: CoRN.algebra.CRings