proposition: Lemma le_absolu : forall x y : Z, (0 <= x)%Z -> (0 <= y)%Z -> (x <= y)%Z -> Z.abs_nat x <= Z.abs_nat y.
proof: Proof. intros [| x| x] [| y| y] Hx Hy Hxy; apply Nat.le_0_l || (try match goal with | id1:(0 <= Zneg _)%Z |- _ => apply False_ind; apply id1; constructor | id1:(Zpos _ <= 0)%Z |- _ => apply False_ind; apply id1; constructor | id1:(Zpos _ <= Zneg _)%Z |- _ => apply False_ind; apply id1; constructor end). simpl in |- *. apply le_inj. do 2 rewrite ZL9. assumption. Qed.
imports: Coq(Lia)