proposition: Lemma posnatMult_1_r : forall p, posnatToNat (posnatMult p (pos 1)) = posnatToNat p.
proof: Proof. intuition. unfold posnatMult. destruct p. remember (pos 1) as p2. destruct p2. unfold posnatToNat. inversion Heqp2; subst. apply Nat.mul_1_r. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms