proposition: Fact nat_ortho_joins_left m n f : m⇣msum nat_join 0 n f = 0 <-> forall i, i < n -> m⇣f i = 0.
proof: Proof. rewrite nat_meet_joins. revert f; induction n as [ | n IHn ]; intros f. + rewrite msum_0; split; auto; intros; lia. + rewrite msum_S, nat_join_eq_0, IHn. split. * intros [ H1 H2 ] [ | i ] ?; auto; apply H2; lia. * intros H; split; intros; apply H; 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)