proposition: Lemma plus_minus : forall a b, cut_minus (a + b) b =N= a.
proof: 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.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.naturals HoTT.Classes.interfaces.orders HoTT.Classes.theory.rings HoTT.Classes.orders.semirings HoTT.Classes.theory.apartness