proposition: Fact binary_le_lb_mask x y : x ≲ y -> ⟬ x ⟭ ⪯ ⟬ y ⟭ .
proof: Proof. induction 1 as [ n | n m H1 H2 IH2 ]. + rewrite nat_lb_fix_0; constructor. + destruct (eq_nat_dec n 0) as [ Hn | Hn ]. - subst; rewrite nat_lb_fix_0; constructor. - assert (n <= m) as Hmn. { apply binary_le_le; constructor; auto. } destruct (euclid_2_div n) as (G1 & [ G2 | G2 ] ); destruct (euclid_2_div m) as (G3 & [ G4 | G4 ] ); try lia. * rewrite G1, G2, G3, G4, Nat.add_0_l, Nat.add_0_l. do 2 (rewrite nat_lb_fix_1; [ | lia ]). constructor; auto. * rewrite G1, G2, G3, G4, Nat.add_0_l, nat_lb_fix_2. rewrite nat_lb_fix_1; [ | lia ]. constructor; auto. * rewrite G1, G2, G3, G4. do 2 rewrite nat_lb_fix_2. constructor; 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)