proposition: Lemma add_rem_idemp_l : forall a b n, n~=0 -> 0 <= a*b -> ((a rem n)+b) rem n == (a+b) rem n.
proof: Proof. assert (Aux : forall a b n, 0<=a -> 0<=b -> n~=0 -> ((a rem n)+b) rem n == (a+b) rem n). { intros a b n **. pos_or_neg n. { apply NZQuot.add_mod_idemp_l; order. } rewrite <- ! (rem_opp_r _ n) by order. apply NZQuot.add_mod_idemp_l; order. } intros a b n Hn Hab. destruct (le_0_mul _ _ Hab) as [(Ha,Hb)|(Ha,Hb)]. { now apply Aux. } apply opp_inj. rewrite <-2 rem_opp_l, 2 opp_add_distr, <-rem_opp_l by order. rewrite <- opp_nonneg_nonpos in *. now apply Aux. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZDiv