In Coq, how do I introduce a variable from an hypothesis into the environment?

Question

Let's say I have made an Hypothesis about the existance of a value. How do I name that variable in the environment?

Example:

Require Import ZArith.
Open Scope Z.
Hint Resolve Zred_factor0 Zmult_assoc_reverse Z.mul_comm Z.mul_add_distr_l
             Z.mul_1_l Z.mul_0_r Z.mul_0_l Z.abs_nonneg.

Definition divides d n := exists c, d*c = n.
Section divisor.

  Variables (d n a:Z).
  Hypothesis H: divides d n.

Now I want to introduce c and the fact that d*c = n into the environment, so I don't have to start my proof by destructing H every time, like this:

  Lemma div4: divides (a*d) (a*n).
    destruct H as [c H'].   (*** Here I would like to already have c and H' *) 
    subst; exists c; auto.  
  Qed.

End divisor.

Answer 1

There is no way of doing what you want, as far as I know. I think it would be a bit complicated to implement because of the restrictions governing Prop elimination.

In this particular case, one thing you could do would be to name n / d as c in your context, and then prove an auxiliary lemma, using your hypothesis, saying that n = c * d. Then you would still have your hypothesis in the statement of your lemmas, but wouldn't have to destruct it all the time.