proposition: Theorem partition_length l l1 l2: partition l = (l1, l2) -> length l = length l1 + length l2.
proof: Proof. revert l1 l2. induction l as [ | a l' Hrec]; intros l1 l2. - now intros [= <- <- ]. - simpl. destruct (f a), (partition l') as (left, right); intros [= <- <- ]; simpl; rewrite (Hrec left right); auto. Qed.
imports: PeanoNat