proposition: Theorem ZdividesZquotientInv : forall n m : Z, n = (Zquotient n m * m)%Z -> Zdivides n m.
proof: Proof. intros n m H'; red in |- *. exists (Zquotient n m); auto. pattern n at 1 in |- *; rewrite H'; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz