proposition: Lemma powerfix'_linearfix: forall n k, pointwise_relation A R (powerfix' n f k) (linearfix (pred (power n)) f k).
proof: Proof. induction n; intros; simpl; intro a. reflexivity. rewrite IHn. rewrite IHn. pose proof (power_positive n). replace (pred (power n + (power n + 0))) with (S (pred (power n) + pred (power n))) by lia. rewrite linearfix_plus. reflexivity. Qed.
imports: ATBR(Common)