forall a b, cut_minus (a + b) b =N= a. Proof. unfold cut_minus,nat_cut_minus. intros a b;revert a;induction b as [|b IH]. - intros [|a];simpl;try split. apply ap,add_0_r. - intros [|a]. + simpl. pose proof (IH 0) as E. rewrite add_0_l in E. exact E. + simpl. change nat_plus with plus. rewrite add_S_r,<-add_S_l;apply IH. Qed.
Require Import