proposition: Lemma add_rem_idemp_r : forall a b n, n~=0 -> 0 <= a*b -> (a+(b rem n)) rem n == (a+b) rem n.
proof: Proof. intros a b n **. rewrite !(add_comm a). apply add_rem_idemp_l; trivial. now rewrite mul_comm. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZDiv