Let A:= (CSetoid_of_less 1).
Fixpoint to_word (n:nat):(list (F 1)):=
match n with
|0 => (@nil (F 1))
|(S m)=> (cons (Build_F 1 0 ZerolessOne)(to_word m))
end.
Definition to_word_: nat_as_CMonoid -> (free_monoid_as_CMonoid A).
Defined.
Lemma to_word_strext: (fun_strext to_word_).
Definition to_word_as_CSetoid_fun:=
(Build_CSetoid_fun nat_as_CSetoid (free_csetoid_as_csetoid A) to_word_ to_word_strext).
Lemma to_word_bijective: (bijective to_word_as_CSetoid_fun).
Lemma pres_plus_to_word:
forall (n m: nat_as_CMonoid),(to_word_ n)[+](to_word_ m)[=](to_word_ (n[+]m)).
End p70text.