proposition: Lemma x_xminone : forall (F : CField) (x : F), x[^]2 [=] x -> x[*] (x[-][1]) [=] [0].
proof: Proof. intros H x h. astepl (x[*]x[-]x[*][1]). astepl (x[*]x[-]x). apply cg_cancel_rht with x. astepl (x[*]x[+][--]x[+]x). astepl (x[*]x[+]([--]x[+]x)). astepl (x[*]x[+][0]). astepl (x[*]x). astepr x. astepl (x[^]2). exact h. Qed.
imports: CoRN.algebra.CRings