proposition: Theorem div_plus : forall n m : nat, 0 < n -> div (n + m) n = 1 + div m n.
proof: Proof. intros n m H; apply sym_equal; apply div_unique; auto. replace (n * (1 + div m n)) with (n + n * div m n); [ apply Nat.add_le_mono_l; apply div_le | ring ]; auto with arith. replace (n * (1 + (1 + div m n))) with (n + n * (1 + div m n)); [ apply Nat.add_lt_mono_l; apply div_lt | ring ]; auto with arith. Qed.
imports: Coq(ArithRing Wf_nat Lia)