intros.
elim k
-[ rewrite < (plus_n_O n).
- simplify.
+[ simplify.
rewrite > H in \vdash (? ? ? %).
rewrite > (H1 ?).
reflexivity
rewrite > sym_plus.
rewrite > (div_plus_times ? ? ? H5).
rewrite > (mod_plus_times ? ? ? H5).
- rewrite > H4.
- simplify.reflexivity.
+ reflexivity.
]
| reflexivity
]
rewrite > sym_plus.
rewrite > (div_plus_times ? ? ? H5).
rewrite > (mod_plus_times ? ? ? H5).
- rewrite > H4.
- simplify.reflexivity.
+ reflexivity.
]
| reflexivity
]