proposition: Fact nat_join_binary_le n m k : n⇡m ≲ k <-> n ≲ k /\ m ≲ k.
proof: Proof. split. + intros H; split; apply binary_le_trans with (2 := H); auto. + intros (H1 & H2). rewrite <- (nat_join_idem k); 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)