proposition: Lemma le_exists : forall n m : nat, iff@{N N N} (n <= m) (sig@{N N} (fun k => m =N= k + n)).
proof: Proof. intros n m;split. - intros E;induction E as [|m E IH]. + exists 0;split. + destruct IH as [k IH]. exists (S k). rewrite IH;reflexivity. - intros [k Hk]. rewrite Hk. apply le_plus. 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