proposition: Theorem DecOptgoodFooPrec_proof n foo : DecOptgoodFooPrec_manual n foo = @decOpt (goodFooPrec n foo) _.
proof: Proof. reflexivity. Qed.
imports: QuickChick(QuickChick Tactics) String mathcomp(ssreflect ssrfun ssrbool ssrnat eqtype seq) List ExtLib.Structures.Monads