proposition: Theorem powerfix_linearfix: forall n k, pointwise_relation A R (powerfix n f k) (linearfix (power n) f k).
proof: Proof. intros. unfold powerfix. setoid_rewrite powerfix'_linearfix. generalize (power_positive n). destruct (power n). intro. lia_false. intro. reflexivity. Qed.
imports: ATBR(Common)