proposition: Lemma no_inverse_Nposmult1 : forall n : Npos, ~ (Npos_mult TWOpos n[=]ONEpos).
proof: Proof. intro n. case n. simpl in |- *. intros. lia. Qed.
imports: CoRN.model.setoids.Nsetoid CoRN.model.structures.Npossec CoRN.algebra.CSetoidFun Coq(Lia)