proposition: Lemma Zdivisor_pos_le : forall a b : Z, (a > 0)%Z -> Zdivides b a -> (a >= b)%Z.
proof: Proof. unfold Zdivides in |- *. intros. elim H0. intros. rewrite <- H1. rewrite Zmult_comm. apply Zmult_pos_mon. rewrite Zmult_comm. rewrite H1. assumption. Qed.
imports: CoRN.model.Zmod.ZBasics