proposition: Lemma implies_neg : tests -> neg_test.
proof: Proof. move=> H. apply/forallInt32P=> x. apply idP. have H': unop_tests x by apply implies_unop. by move: H'=> /andP [_ /andP [_ /andP [H1 _]]]. Qed.
imports: Coq(ZArith.ZArith Extraction) mathcomp.ssreflect.ssreflect mathcomp(ssrbool eqtype ssrnat seq fintype ssrfun tuple) Bits(bits) ExtrOcamlBasic