proposition: Lemma nexp_two : forall x : R, x[^]2 [=] x[*]x.
proof: Proof. intro x. replace 2 with (1 + 1). Step_final (x[^]1[*]x[^]1). auto with arith. Qed.
imports: CoRN.tactics.CornTac CoRN.algebra.CSums CoRN.algebra.CAbMonoids Coq.Sorting.Permutation CoRN.util.SetoidPermutation Coq.Setoids.Setoid Coq.Classes.Morphisms Coq(Lia)