proposition: Lemma powerfix'_linearfix: forall n k, powerfix' n f k = linearfix (pred (pow2 n)) f k.
proof: Proof. induction n; intros. reflexivity. rewrite pred_pow2_Sn. simpl. now rewrite <-linearfix_double, 2IHn. Qed.
imports: common