proposition: Lemma rem_add : forall a b c, c~=0 -> 0 <= (a+b*c)*a -> (a + b * c) rem c == a rem c.
proof: Proof. assert (forall a b c, c~=0 -> 0<=a -> 0<=a+b*c -> (a+b*c) rem c == a rem c). { intros a b c **. pos_or_neg c. - apply NZQuot.mod_add; order. - rewrite <- (rem_opp_r a), <- (rem_opp_r (a+b*c)) by order. rewrite <- mul_opp_opp in *. apply NZQuot.mod_add; order. } intros a b c Hc Habc. destruct (le_0_mul _ _ Habc) as [(Habc',Ha)|(Habc',Ha)]. { auto. } apply opp_inj. revert Ha Habc'. rewrite <- 2 opp_nonneg_nonpos. rewrite <- 2 rem_opp_l, opp_add_distr, <- mul_opp_l by order. auto. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZDiv