proposition: Lemma lsl_repr: forall i j bs k, k <= wordsize -> native_repr i bs -> natural_repr j k -> native_repr (lsl i j) (shlBn bs k).
proof: Proof. move=> i i' ? k ltn_k. rewrite /native_repr eq_adj; move/eqP=> <-. rewrite /natural_repr. move/existsP=> [bs' /andP [H /eqP H']]. rewrite /native_repr eq_adj in H. move/eqP: H=> H. apply/eqInt16P. have Hk: k = toNat (bitsFromInt16 i'). rewrite H. have ->: k = toNat (fromNat (n := wordsize) k). rewrite toNat_fromNatBounded=> //. by apply (leq_ltn_trans (n := wordsize)). by rewrite H'. rewrite Hk. rewrite Hk in ltn_k. clear H H' Hk. move: i' ltn_k; apply/(forallInt16P (fun i' => (toNat (bitsFromInt16 i') <= wordsize) ==> (eq (lsl i i') (bitsToInt16 (shlBn (bitsFromInt16 i) (toNat ((bitsFromInt16 i')))))))). move=> i'. apply/equivP. apply/implyP. split=> H H'. move: (H H')=> H''. by apply/eqInt16P. move: (H H')=> H''. by apply/eqInt16P. move: i; apply/forallInt16P; last by apply lsl_valid. move=> i'; apply idP. Qed.
imports: Coq(ZArith.ZArith Extraction) mathcomp.ssreflect.ssreflect mathcomp(ssrbool eqtype ssrnat seq fintype ssrfun tuple) Bits(bits)