proposition: Lemma relation_shift {X : Metric_Space} (a : nat -> Base X) (k : nat) (n : nat) (n_ge_k : (n ≥ k)%nat) : a ((n - k) + k)%nat = a n.
proof: Proof. We conclude that (a (n - k + k) = a n)%nat. Qed.
imports: Coq.Reals.Reals Automation Libs.Negation Notations Tactics