proposition: Lemma div_le_upper_bound : forall a b q, a <= b*q -> a/b <= q.
proof: Proof. intros a b c. destruct (eq_decidable b 0) as [->|Hb]. - nzsimpl. intros. apply le_0_l. - now apply div_le_upper_bound. Qed.
imports: NAxioms NSub NDiv