proposition: Lemma chain_le : transitive R -> reflexive R -> forall f x y, chain f -> x <= y -> R (f x) (f y).
proof: Proof. intros Ht Hr f x y Hc H; induction H; eauto. Qed.
imports: Relations Classical ClassicalEpsilon Zwf Compare_dec List ZArith