proposition: Lemma decreasing_seqP (d : unit) (T : porderType d) (u_ : T ^nat) : (forall n, u_ n > u_ n.+1)%O <-> decreasing_seq u_.
proof: Proof. split. move=> u_noninc. apply: (@total_homo_mono _ T u_ leq ltn _ _ leqnn _ ltn_neqAle _ (fun _ _ _ => esym (le_anti _)) leq_total (homo_ltn (fun _ _ _ u v => lt_trans v u) u_noninc)) => //. by move=> x y; rewrite eq_sym -lt_neqAle. by move=> u_decr n; rewrite lt_neqAle eq_le !u_decr !leqnSn ltnn. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum matrix) mathcomp(interval rat) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(set_interval) reals ereal signed topology normedtype landau