proposition: Lemma prod_length : forall (l:list A)(l':list B), length (list_prod l l') = (length l) * (length l').
proof: Proof. intro l; induction l as [|? ? IHl]; simpl; [easy|]. intros. now rewrite app_length, map_length, IHl. Qed.
imports: PeanoNat