fact: Definition raster_well_formed {columns lines : positive} (r : raster columns lines) : Prop := match r with raster_data _ _ d => length d = Pos.to_nat lines /\ Forall (fun line : list bool => length line = Pos.to_nat columns) d end.
imports: CoRN.stdlib_omissions.List Coq.Arith.Arith Coq.PArith.BinPos