proposition: Lemma monS : (forall x, ltA (f x) (f (S x))) -> (forall x y, x < y -> ltA (f x) (f y)).
proof: Proof. intros hf x. cut (forall k, ltA (f x) (f (k+S x))). intros hx y xy. assert (y = (y-S x)+S x). lia. rewrite H. apply hx. induction k; simpl. apply hf. apply ht with (f (k+S x)). hyp. apply hf. Qed.
imports: Coq(Morphisms Euclid Peano Lia) Coq(Compare) CoLoR(LogicUtil EqUtil BoolUtil NatCompat RelUtil)