proposition: Fact nat_ortho_plus_join n m : n⇣m = 0 -> n+m = n⇡m.
proof: Proof. do 2 rewrite equal_lb_mask_equiv. unfold nat_meet, nat_join. do 2 rewrite nat_lb_nat. rewrite nat_lb_plus, nat_lb_fix_0. rewrite <- lb_ortho_meet_nil. apply lb_ortho_plus_join. 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)