proposition: Lemma lub_lift_reverse : forall (c:nat->A->B)(l:A->B), lub lift_order l c -> forall x, lub R (l x)(fun n => c n x).
proof: Proof. intros c l [Hub Hl] x. split. intros n; apply (Hub n x). intros b' Hup'. assert (Hupg' : upper_bound lift_order (p_v l x b') c). intros n y; case (classic (y=x)). intros Hyx; subst y; rewrite pointwise_variant_eq; apply Hup'. intros Hn; rewrite pointwise_variant_diff; auto; apply Hub. rewrite <- (pointwise_variant_eq l x b'); apply Hl; assumption. Qed.
imports: Relations Classical ClassicalEpsilon Zwf Compare_dec List ZArith