proposition: Lemma lt_sum (x y : positive) : x < y ↔ ∃ z, y = x + z.
proof: Proof. split. - exists (y - x)%positive. symmetry. apply Pplus_minus. lia. - intros [z ->]. lia. Qed.
imports: Coq(QArith Qcanon) stdpp(well_founded) stdpp(options)