proposition: Lemma div_imp_leq : forall a b : Z_as_CRing, b [#] [0] -> Zdivides a b -> Z.abs_nat a <= Z.abs_nat b.
proof: Proof. intros a b Hap Hdiv. destruct Hdiv. rewrite <- H. rewrite Zabs_nat_mult. rewrite <- H in Hap. destruct x. destruct Hap. reflexivity. simpl. destruct (ZL4 p). rewrite H0. simpl. rewrite <- (Nat.add_0_r (Z.abs_nat a)) at 1. apply Nat.add_le_mono_l. apply Nat.le_0_l. simpl. destruct (ZL4 p). rewrite H0. simpl. rewrite <- (Nat.add_0_r (Z.abs_nat a)) at 1. apply Nat.add_le_mono_l. apply Nat.le_0_l. Qed.
imports: Zring Qring Q_can