-(*
-theorem sum_div_eq_div: \forall a,b,c:nat.
-O \lt c \to b \lt c \to c \divides a \to (a+b) /c = a/c.
-intros.
-elim H2.
-rewrite > H3.
-rewrite > (sym_times c n2).
-rewrite > (div_plus_times c n2 b)
-[ rewrite > (div_times_ltO n2 c)
- [ reflexivity
- | assumption
- ]
-| assumption
-]
-qed.
-*)