proposition: Fact nat_ortho_sum_join n f : (forall i j, i <> j -> i < n -> j < n -> f i ⇣ f j = 0) -> ∑ n f = msum nat_join 0 n f.
proof: Proof. revert f; induction n as [ | n IHn ]; intros f Hf. + do 2 rewrite msum_0; auto. + do 2 rewrite msum_S. rewrite IHn. apply nat_ortho_plus_join, nat_ortho_joins_left. * intros; apply Hf; lia. * intros; apply Hf; 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)