proposition: Lemma implies_shift : tests -> forall x y, toNat (bitsFromInt8 x) <= wordsize -> shift_tests x (toNat (bitsFromInt8 x)) y (bitsFromInt8 y).
proof: Proof. move => H x y Hlt. move: (implies_unop H x)=> /andP [_ /andP [_ /andP [_ /andP [_ /andP [H1 _]]]]]. rewrite Hlt in H1. have Hb: (binop_tests x (bitsFromInt8 x) y (bitsFromInt8 y)) && (shift_tests x (toNat (bitsFromInt8 x)) y (bitsFromInt8 y)). move: H1=> /forallInt8P H1. move: (H1 (fun y => (binop_tests x (bitsFromInt8 x) y (bitsFromInt8 y)) && (shift_tests x (toNat (bitsFromInt8 x)) y (bitsFromInt8 y))))=> H2. apply H2=> y'. by apply idP. by move: Hb=> /andP [_ ->]. Qed.
imports: Coq(ZArith.ZArith Extraction) mathcomp.ssreflect.ssreflect mathcomp(ssrbool eqtype ssrnat seq fintype ssrfun tuple) Bits(bits) ExtrOcamlBasic