proposition: Lemma succ_abs_eq_abs_one_plus : forall (x:int), x >= 0 -> S (abs x) = abs (1 + x) :> nat.
proof: Proof. Proof using. intros x. pattern x. applys (@measure_induction _ abs). clear x. intros x IH Pos. rewrite <- Zabs_nat_Zsucc. fequals. math. math. Qed.
imports: Coq.ZArith.ZArith TLC(LibTactics LibLogic LibReflect LibRelation)