proposition: Lemma ltInRange : forall m n, le n m -> n <> O -> In n (rangeNat m).
proof: Proof. induction m; intros. + inversion H. simpl. auto. + simpl. inversion H. - left; auto. - right; subst. apply IHm; auto. Qed.
imports: PArith List ChoiceFacts Lia mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool) Classes RandomQC Generators Sets