proposition: Lemma dnn_alt (s : ∞A) : DecreasingNonNegative s ↔ ForAll (λ s, ForAll (λ t, 0 ≤ hd t ≤ hd s) s) s.
proof: Proof. split; revert s; cofix FIX; intros s E. constructor. cut (hd s ≤ hd s); [|reflexivity]. set (x:=hd s). unfold x at 1. generalize s E x. clear s E x. cofix FIX2. intros s E. constructor. split; trivial. destruct E. now transitivity (hd (tl s)). destruct E. apply FIX2; trivial. now transitivity (hd s). destruct E. now apply FIX. constructor. now destruct E as [[? [? ?]] ?]. apply FIX. now destruct E. Qed.
imports: Coq.setoid_ring.Ring Coq.Arith.Factorial MathClasses.misc.workaround_tactics MathClasses.interfaces.abstract_algebra MathClasses.interfaces.additional_operations MathClasses.interfaces.orders MathClasses.interfaces.naturals MathClasses.interfaces.integers MathClasses.theory.nat_pow MathClasses.theory.int_pow MathClasses.theory.streams