proposition: Fact lb_ortho_plus_id a x y : a ⟂ x -> a ⟂ y -> x ⟂ y <-> (a⊕x)↓(a⊕y) ≂ a.
proof: Proof. intros H1 H2. do 2 (rewrite lb_ortho_plus_join; auto). rewrite <- lb_join_meet_distr, lb_ortho_meet_nil. split. + intros H3; rewrite H3, lb_join_left; auto. + intros H3; apply lb_ortho_mask_nil with a. * revert H1; apply lb_ortho_anti; auto. * rewrite <- H3, lb_join_comm; 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)