proposition: Lemma left_id_injection: forall {S T : Type} (f: S -> T) (g: T-> S), left_identity f g -> injection f.
proof: Proof. introv lid feq. apply_eq g feq ffeq. rw lid in ffeq. rw lid in ffeq. trivial. Qed.
imports: Coq.Init.Notations tactics Peano Basics Bool Arith Arith.EqNat Omega