proposition: Lemma x_apply : forall x : R, _X_ ! x [=] x.
proof: Proof. intros. simpl in |- *. astepl (x[*]([1][+]x[*][0])). astepl (x[*]([1][+][0])). astepl (x[*][1]). algebra. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational