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