proposition: Fact lb_ortho_plus l m : l ⟂ m <-> l ⪯ l⊕m.
proof: Proof. split. + induction 1 as [ l | l | x y l m [ H1 | H1 ] H2 IH2 ]. * constructor. * rewrite lb_plus_fix_1. rewrite lb_mask_eq_binary_le, lb_succ_spec; simpl. rewrite <- lb_mask_eq_binary_le; apply lb_mask_refl. * rewrite lb_plus_fix_2. subst x; rewrite bin_add_eq_00x. destruct y; constructor; auto. * rewrite lb_plus_fix_2. subst y; rewrite bin_add_eq_0x0. destruct x; constructor; auto. + revert m; induction l as [ | x l IHl ]. * intros; constructor. * intros [ | y m ] H. - constructor. - rewrite lb_plus_fix_2 in H. destruct x; destruct y; simpl in H; try (apply lb_mask_inv_cons_cons in H; tauto); apply lb_mask_inv_cons, proj2 in H; 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)