proposition: Lemma to_word_bijective: (bijective to_word_as_CSetoid_fun).
proof: Proof. unfold bijective. split. unfold injective. simpl. intros a0. induction a0. intro a1. case a1. unfold ap_nat. intuition. simpl. intuition. intro a1. case a1. simpl. intuition. intros n H. unfold ap_nat in H. simpl. right. apply IHa0. unfold ap_nat. intro H1. rewrite H1 in H. apply H. reflexivity. unfold surjective. simpl. unfold Astar. unfold A. intro b. induction b. exists 0. simpl. exact I. elim IHb. intros c H. exists (S c). split. simpl in a. elim a. simpl. intuition. exact H. Qed.
imports: Lia CoRN.algebra.CMonoids CoRN.model.monoids.Nmonoid CoRN.model.setoids.Nfinsetoid