{x y: N}: x ≤ y <-> exists z, y = x + z. Proof. split; intros E. - destruct (decompose_le E) as [z [Ez1 Ez2]]. exists z. trivial. - destruct E as [z Ez]. apply compose_le with z; [solve_propholds | trivial]. Qed.
Require Import Require Import Require Import