proposition: Lemma app_right_reg : forall l l1 l2:list A, l1 ++ l = l2 ++ l -> l1 = l2.
proof: Proof. intros l l1 l2 e. assert (H: rev (l1 ++ l) = rev (l2 ++ l)). - now rewrite e. - repeat rewrite rev_app in H. generalize (app_left_reg _ _ _ H). intro H1; rewrite <- (rev_involutive l1) ; rewrite <- (rev_involutive l2); rewrite H1; auto. Qed.
imports: List Arith Lia