proposition: Lemma square_eq : forall x a : F, a [#] [0] -> x[^]2 [=] a[^]2 -> {x [=] a} + {x [=] [--]a}.
proof: Proof. intros x a a_ H. elim (cond_square_eq F x a); auto. apply two_ap_zero. Qed.
imports: CoRN.tactics.FieldReflection CoRN.tactics.Rational CoRN.algebra.CSetoids Coq(Lia)