proposition: Fact nat_join_mono a b u v : a ≲ b -> u ≲ v -> a⇡u ≲ b⇡v.
proof: Proof. do 3 rewrite binary_le_eq_lb_mask; unfold nat_join. do 2 rewrite nat_lb_nat. apply lb_join_mono. 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)