proposition: Lemma listAppNeq : forall (A : Type) (l1 l2 l3 l4 : list A), (forall (x y : A), {x = y} + {x <> y}) -> length l1 = length l2 -> l1 <> l2 -> l1 ++ l3 <> l2 ++ l4.
proof: Proof. induction l1. + intros. destruct l2. - unfold not in H0. exfalso; apply H0; auto. - simpl in H; inversion H. + intros l2 l3 l4 EqDec Len Neq. destruct l2 as [ | b l2 ]. - simpl in Len. congruence. - destruct (EqDec a b). * subst. simpl in Len. inversion Len as [ Len']; clear Len. simpl. pose proof (IHl1 l2 l3 l4 EqDec Len') as Contra; clear IHl1. assert (l1 <> l2) by (unfold not; intros; congruence). apply Contra in H. unfold not in *. intros. apply H. inversion H0. auto. * unfold not; intros. inversion H. congruence. Qed.
imports: PArith List ChoiceFacts Lia mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool) Classes RandomQC Generators Sets