proposition: Lemma le_inversion : forall (x y:nat) (P:le x y), (exists H:x=y, P = (eq_rect x (le x) (le_n x) y H)) \/ (exists y':nat, exists R:(S y') = y, exists H:(le x y'), P = (eq_rect (S y') (le x) (le_S x y' H) y R)).
proof: Proof. intros x y P. case P. left. exists (eq_refl x); auto. intros m H. right. exists m. exists (eq_refl (S m)). exists H; auto. Qed.
imports: Coq(Lia List Setoid Peano_dec Eqdep_dec Ring Zwf Morphisms ZArith) CoLoR(interp)