Skip to content

Instantly share code, notes, and snippets.

@yoshihiro503

yoshihiro503/SsreflectTutorial_3.4_edivnP_left.v

Created July 26, 2014 06:07
Show Gist options
  • Save yoshihiro503/d1d2a58c6a6eed517344 to your computer and use it in GitHub Desktop.
Save yoshihiro503/d1d2a58c6a6eed517344 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
SsreflectTutorial_3.4_edivnP_left.v
Lemma edivnP_left : forall m d, edivn_spec_left m d (edivn m d).
Proof.
move=> m d.
case: (edivnP m d) => q r eq impl.
by apply EdivnSpec_left.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment