proposition: Lemma Zabs_Zminus_symm : forall a b : Z, Z.abs (a - b) = Z.abs (b - a).
proof: Proof. intros a b. replace (a - b)%Z with (- (b - a))%Z by auto with zarith. apply Zabs_Zopp. Qed.
imports: Coq.ZArith.ZArith CoRN.logic.CLogic Coq(Lia)