proposition: Lemma increasing_seq_prop f r: order r -> function f -> source f = Nat -> sub (target f) (substrate r) -> (forall n, natp n -> gle r (Vf f n) (Vf f (csucc n))) -> increasing_sequence (graph f) r.
proof: Proof. move => or ff sf tf ale. split;fprops; rewrite ? domain_fg //. apply: (@sub_trans (target f)) => //; apply: f_range_graph=>//. move=> n m nN mN /cdiff_pr <-. rewrite -/(Vf _ _ ) -/(Vf _ _). move: (m -c n) (NS_diff n mN); apply: Nat_induction. by rewrite (Nsum0r nN); order_tac; apply: tf; Wtac;rewrite sf. move=> p pN le1. rewrite (csum_nS _ pN); move: (ale _ (NS_sum nN pN))=> le2; order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)