Commit 927a2930 authored by Ralf Jung's avatar Ralf Jung
Browse files

tweak proof to also work after a Coq bugfix

parent 0dec8845
......@@ -74,7 +74,7 @@ Section ufrac_auth.
rewrite auth_both_validN=> -[Hincl Hvalid].
move: Hincl=> /Some_includedN=> -[[_ ? //]|[[[p' ?] ?] [/=]]].
move=> /discrete_iff /leibniz_equiv_iff; rewrite ufrac_op'=> [/Qp_eq/=].
rewrite -discrete_iff leibniz_equiv_iff. rewrite ufrac_op'=> [/Qp_eq/=].
rewrite -{1}(Qcplus_0_r p)=> /(inj (Qcplus p))=> ?; by subst.
Lemma ufrac_auth_agree p a b : (U{p} a U{p} b) a b.
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment