proposition: Lemma step_eq lss : sizeof_pair (step lss) = sizeof_pair lss -> step lss = lss.
proof: Proof. unfold sizeof_pair, step; simpl. destruct lss as [lsA lsB]; simpl. intro H. repeat match goal with | [ H : context[filter ?f ?ls] |- _ ] => unique pose proof (length_filter f ls) end. match goal with | [ H : ?x + ?y = ?x' + ?y' |- _ = _ :> list _ * list _ ] => assert (x = x') by omega; assert (y = y') by omega; clear H end. rewrite !length_filter_eq by omega. reflexivity. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Arith.EqNat Coq.Arith.Compare_dec Coq.ZArith.ZArith Coq.Lists.List Fiat.Common.List.ListFacts Fiat.Common