proposition: Lemma inj_mod x y : Z.of_nat (x `mod` y) = (Z.of_nat x) `mod` (Z.of_nat y).
proof: Proof. destruct (decide (y = 0%nat)); [by subst; destruct x |]. apply Z.mod_unique with (Z.of_nat $ x `div` y)%nat. { left. rewrite <-(Nat2Z.inj_le 0), <-Nat2Z.inj_lt. apply Nat.mod_bound_pos; lia. } by rewrite <-Nat2Z.inj_mul, <-Nat2Z.inj_add, <-Nat.div_mod. Qed.
imports: Coq(QArith Qcanon) stdpp(well_founded) stdpp(options)