proposition: Lemma carac_monotonic : forall (A B:Type)(P:A -> Prop)(Q:B->Prop)(Pdec: dec P)(Qdec: dec Q) x y, (P x -> Q y) -> carac Pdec x <= carac Qdec y.
proof: Proof. intros; unfold carac; case (Pdec x); intros; auto. case (Qdec y); intros; auto. absurd (Q y); auto. Qed.
imports: ALEA(Utheory) ALEA(Sets)