forall a b : nat, iff@{N N N} (a <= b) (S a <= S b). 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.
Require Import