proposition: Lemma le_plus : forall n k, n <= k + n.
proof: Proof. induction k. - apply Nat.Core.leq_n. - simpl_nat. constructor. assumption. 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