proposition: Lemma nb_elts_lt_le : forall k n, (k <= n)%nat -> nb_elts (lt_dec k) n = k.
proof: Proof. intros k n H; induction H; intros; auto with arith. simpl. case (lt_dec k m); intros; auto with arith. absurd ((m<k)%nat); auto with arith. Qed.
imports: ALEA(Utheory) ALEA(Sets)