proposition: Fact binary_le_joins_inv m n f : m ≲ msum nat_join 0 n f -> { k : nat & { g : nat -> nat & { h | m = msum nat_join 0 k g /\ k <= n /\ (forall i, i < k -> g i <> 0 /\ g i ≲ f (h i)) /\ (forall i, i < k -> h i < n) /\ (forall i j, i < j < k -> h i < h j) } } }.
proof: Proof. revert m f; induction n as [ | n IHn ]; intros m f H. + rewrite msum_0 in H; apply binary_le_zero_inv in H. subst; exists 0, (fun _ => 0), (fun _ => 0); split. - rewrite msum_0; auto. - split; [ | split; [ | split ] ]; intros; lia. + rewrite msum_S in H. apply binary_le_join_inv in H. destruct (@IHn (m ⇣ msum nat_join 0 n (fun n => f (S n))) (fun n => f (S n))) as (k & g & h & H1 & H0 & H2 & H3 & H4); auto. rewrite H1 in H. case_eq (m ⇣ f 0). * intros E. rewrite E, nat_join_0n in H. exists k, g, (fun i => S (h i)); repeat (split; auto). - intros i Hi; specialize (H3 _ Hi); lia. - intros i j Hij; specialize (H4 _ _ Hij); lia. * intros u Hu. exists (S k), (fun i => match i with 0 => S u | S i => g i end), (fun i => match i with 0 => 0 | S i => S (h i) end); split; [ | split; [ | split; [ | split ] ] ]. - rewrite H, msum_S, <- Hu; auto. - lia. - intros [ | i ]; split; try lia. ++ rewrite <- Hu; auto. ++ apply H2; lia. ++ apply H2; lia. - intros [ | i ] Hi; try lia. apply Nat.succ_lt_mono, H3 in Hi; lia. - intros [ | i ] [ | j ] (G1 & G2); simpl; try lia. apply -> Nat.succ_lt_mono. apply H4; 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)