fact: Definition bool_add_with_rem a b c : bool * bool := match a, b, c with | ⟘, ⟘, ⟘ => (⟘,⟘) | ⟘, ⟘, ⟙ => (⟘,⟙) | ⟘, ⟙, ⟘ => (⟘,⟙) | ⟘, ⟙, ⟙ => (⟙,⟘) | ⟙, ⟘, ⟘ => (⟘,⟙) | ⟙, ⟘, ⟙ => (⟙,⟘) | ⟙, ⟙, ⟘ => (⟙,⟘) | ⟙, ⟙, ⟙ => (⟙,⟙) end.
imports: Arith Nat Lia List Bool Setoid Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat bool_list gcd sums power_decomp)