proposition: Lemma chain_lift_reverse : forall c, chain lift_order c -> forall x, chain R (fun n => c n x).
proof: Proof. intros c Hch x n; apply (Hch n x). Qed.
imports: Relations Classical ClassicalEpsilon Zwf Compare_dec List ZArith