proposition: Fact F2 : x <= y.
proof: Proof. unfold y in *; clear y; induction x. - auto with arith. - assert (m (iota n) < m (iota (S n))). { apply mDecr; unfold iota; simpl. split. - constructor. - split. + constructor 2; auto with arith. + constructor. } lia. Qed.
imports: Relations List Sorted Arith hydras(Restriction) Coq(Lia)