proposition: Lemma pres_plus_to_word: forall (n m: nat_as_CMonoid),(to_word_ n)[+](to_word_ m)[=](to_word_ (n[+]m)).
proof: Proof. simpl. intros n m. induction n. simpl. apply eq_fm_reflexive. simpl. intuition. Qed.
imports: Lia CoRN.algebra.CMonoids CoRN.model.monoids.Nmonoid CoRN.model.setoids.Nfinsetoid