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