proposition: Lemma plus_inv_zero_l: forall y x, x + y = y -> x = 0.
proof: Proof. induction y; intros. { rewrite plus_comm in H. assumption. } destruct x. { simpl in *. reflexivity. } rewrite Nat.add_succ_r in H. inversion H; subst; clear H. apply IHy. assumption. Qed.
imports: Coq.Arith.Plus Coq.Arith.PeanoNat Coq.Lists.List