proposition: Lemma getBit_liftBinOp: forall n op (bs: BITS n)(bs': BITS n) k, k < n -> getBit (liftBinOp op bs bs') k = op (getBit bs k) (getBit bs' k).
proof: Proof. elim=> // n IHn op /tupleP[b bs] /tupleP[b' bs']; case=> [|k] ?. + have ->: getBit (liftBinOp op [tuple of b :: bs] [tuple of b' :: bs']) 0 = op b b' by compute. by trivial. + have ->: getBit [tuple of b :: bs] k.+1 = getBit bs k by compute. have ->: getBit [tuple of b' :: bs'] k.+1 = getBit bs' k by compute. have ->: getBit (liftBinOp op [tuple of b :: bs] [tuple of b' :: bs']) k.+1 = getBit (liftBinOp op bs bs') k by compute. by apply IHn. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype tuple zmodp div) ssrextra.tuple ssrextra.nat spec spec.properties operations