proposition: Lemma mul_rem_idemp_l : forall a b n, n~=0 -> ((a rem n)*b) rem n == (a*b) rem n.
proof: Proof. assert (Aux1 : 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.mul_mod_idemp_l; order. - rewrite <- ! (rem_opp_r _ n) by order. apply NZQuot.mul_mod_idemp_l; order. } assert (Aux2 : forall a b n, 0<=a -> n~=0 -> ((a rem n)*b) rem n == (a*b) rem n). { intros a b n **. pos_or_neg b. - now apply Aux1. - apply opp_inj. rewrite <-2 rem_opp_l, <-2 mul_opp_r by order. apply Aux1; order. } intros a b n Hn. pos_or_neg a. { now apply Aux2. } apply opp_inj. rewrite <-2 rem_opp_l, <-2 mul_opp_l, <-rem_opp_l by order. apply Aux2; order. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZDiv