proposition: Fact F1 : y < x.
proof: Proof. apply mDecr; unfold x,iota; cbn. split. - red; constructor. - split. + constructor; auto with arith. + red; constructor. Qed.
imports: Relations List Sorted Arith hydras(Restriction) Coq(Lia)