proposition: Fact nat_lb_length x n : x < power n 2 -> length ⟬ x ⟭ <= n.
proof: Proof. revert x; induction n as [ | n IHn ]; intros x. + rewrite power_0; intro; replace x with 0; try lia. rewrite nat_lb_fix_0; simpl; lia. + rewrite power_S. destruct (euclid_2 x) as (y & [ H | H ]); intros Hx; subst. * destruct y. - simpl; rewrite nat_lb_fix_0; simpl; lia. - rewrite nat_lb_fix_1; try lia. simpl; apply le_n_S, IHn; lia. * rewrite nat_lb_fix_2; simpl. apply le_n_S, IHn; 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)