proposition: Lemma le_S_S : forall a b : nat, iff@{N N N} (a <= b) (S a <= S b).
proof: Proof. intros. etransitivity;[apply le_exists|]. etransitivity;[|apply symmetry,le_exists]. split;intros [k E];exists k. - rewrite E,add_S_r. reflexivity. - rewrite add_S_r in E;apply (injective _) in E. trivial. 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