proposition: Fact sum_powers_ortho n f e : (forall i, i < n -> f i < r) -> (forall i j, i < n -> j < n -> e i = e j -> i = j) -> sum_powers r n f e = ⇧ r n f e.
proof: Proof. Proof using Hq Hr. revert f e; induction n as [ | n IHn ]; intros f e H1 H2. + do 2 rewrite msum_0; auto. + rewrite msum_S. rewrite IHn. 2: intros; apply H1; lia. 2: intros i j Hi Hj E; apply H2 in E; lia. rewrite nat_ortho_plus_join. * rewrite msum_S; auto. * apply nat_ortho_joins_left. intros i Hi. apply nat_meet_powers_neq. - intros E; apply H2 in E; lia. - apply H1; lia. - apply H1; lia. Qed.
imports: Arith Nat Lia List Bool Setoid Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat bool_list gcd sums power_decomp)