proposition: Fact lb_ortho_plus_join x y : x ⟂ y -> x⊕y ≂ x↑y.
proof: Proof. induction 1 as [ m | l | x y l m H1 H2 IH2 ]. + rewrite lb_plus_fix_0, lb_join_right; apply lb_succ_bot. + rewrite lb_plus_fix_1, lb_join_left; apply lb_succ_bot. + rewrite lb_join_cons. apply lb_mask_equiv_equal. rewrite lb_plus_spec_0. do 3 rewrite lb_nat_fix_3. rewrite lb_mask_equiv_equal in IH2. rewrite <- IH2. rewrite lb_plus_spec_0. destruct x; destruct y; simpl; try ring. destruct H1; discriminate. 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)