proposition: Lemma modn_sub : forall N x y, 0 < N -> x < N -> y < N -> N <= x+y -> (x + y) %% N + N = x+y.
proof: Proof. move => N x y B H1 H2 H3. assert (H4:= divn_eq (x+y) N). rewrite {2}H4. rewrite addnC. assert (LT:(x + y) %/ N < 2). rewrite ltn_divLR. rewrite mul2n -addnn. rewrite -(ltn_add2r y) in H1. apply (ltn_trans H1). by rewrite ltn_add2l. done. assert (GT:0 < (x + y) %/ N). by rewrite divn_gt0. rewrite ltnS in LT. assert (1 <= (x+y) %/ N <= 1). by rewrite GT LT. rewrite -eqn_leq in H. rewrite -(eqP H). by rewrite mul1n. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype tuple zmodp div)