proposition: Corollary flat_map_constant_length A B c (f: A -> list B) l: (forall x, In x l -> length (f x) = c) -> length (flat_map f l) = (length l) * c.
proof: Proof. intro H. rewrite flat_map_length. induction l as [ | a l IHl ]; [reflexivity|]. simpl. rewrite IHl, H; [reflexivity | left; reflexivity | ]. intros x Hx. apply H. right. assumption. Qed.
imports: PeanoNat