proposition: Lemma le_plus_minus : forall n m : nat, n <= m -> m =N= (n + (cut_minus m n)).
proof: Proof. intros n m E. apply le_exists in E. destruct E as [k E];rewrite E. rewrite plus_minus. apply add_comm. 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