fact: Definition isNone {T : Type} (u : option T) := match u with | Some _ => false | None => true end.
imports: ZArith List Lia mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat seq eqtype) QuickChick(Sets Tactics RandomQC)