proposition: Lemma remove_length_lt {A R} {_ : @Equivalence A R} (dec : forall x y, {R x y} + {~R x y}) (ls ls' : list A) x (H0 : InA R x ls) (H1 : ~InA R x ls') (Hls : NoDupA R ls) (Hls' : NoDupA R ls') (H2 : forall y, (InA R y ls /\ ~R y x) <-> InA R y ls') : List.length ls' < List.length ls.
proof: Proof. hnf. erewrite <- remove_length_eq_S; [ reflexivity | .. ]; try eassumption. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Coq.Lists.List Coq.Lists.SetoidList Coq.Bool.Bool Fiat.Common Fiat.Common.List.Operations Fiat.Common.Equality Fiat.Common.List.FlattenList Fiat.Common.LogicFacts