proposition: Lemma lift_associative op n : associative op -> associative (liftBinOp (n:=n) op).
proof: Proof. by lift_op_t n. 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