proposition: Lemma rangeNatLt : forall n m, In m (rangeNat n) -> lt m (S n) /\ m <> O.
proof: Proof. induction n; intros. + simpl in H. inversion H. + inversion H. - split. * subst. unfold lt. apply le_n. * congruence. - apply IHn in H0; inversion H0; clear H0; split. * unfold lt in *. apply le_S. auto. * auto. Qed.
imports: PArith List ChoiceFacts Lia mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool) Classes RandomQC Generators Sets