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