proposition: Lemma mod_minus a b : b <> 0 -> b < a -> (a - b) mod b = a mod b.
proof: Proof. intros. replace a with ((a - b) + b) at 2 by lia. rewrite <- Nat.Div0.add_mod_idemp_r; auto. rewrite Nat.Div0.mod_same; auto. Qed.
imports: Equations(Equations) Relations Arith Lia ExtrOcamlBasic