proposition: Fact nat_ortho_joins m n f g : msum nat_join 0 m f ⇣ msum nat_join 0 n g = 0 <-> forall i j, i < m -> j < n -> f i ⇣ g j = 0.
proof: Proof. rewrite nat_ortho_joins_left. split; intros H. + intros i j H1 H2; specialize (H _ H2). rewrite nat_meet_comm in H |- *. rewrite nat_ortho_joins_left in H; auto. + intros i Hi; rewrite nat_meet_comm, nat_ortho_joins_left. intros j Hj; rewrite nat_meet_comm; auto. 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)