proposition: Lemma inj_mod: forall (a b: N), (b <> 0)%N -> N.to_nat (a mod b)%N = (N.to_nat a) mod (N.to_nat b).
proof: Proof. intros. rewrite <-? N_to_Z_to_nat. rewrite N2Z.inj_mod by assumption. apply Nat2Z.inj. rewrite Nat2Z.inj_mod. rewrite? Z2Nat.id; try apply N2Z.is_nonneg. - reflexivity. - pose proof (Z.mod_pos_bound (Z.of_N a) (Z.of_N b)) as Q. destruct Q as [Q _]. + destruct b; try contradiction. simpl. constructor. + exact Q. Qed.
imports: Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop Coq.Arith.Arith Coq.NArith.NArith Coq.ZArith.ZArith Coq.micromega.Lia