Commit e6f6758c authored by Ralf Jung's avatar Ralf Jung

tweak proof to also work after a Coq bugfix

parent f455b5d4
Pipeline #18358 failed with stage
in 0 seconds
...@@ -74,7 +74,7 @@ Section ufrac_auth. ...@@ -74,7 +74,7 @@ Section ufrac_auth.
Proof. Proof.
rewrite auth_both_validN=> -[Hincl Hvalid]. rewrite auth_both_validN=> -[Hincl Hvalid].
move: Hincl=> /Some_includedN=> -[[_ ? //]|[[[p' ?] ?] [/=]]]. 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. rewrite -{1}(Qcplus_0_r p)=> /(inj (Qcplus p))=> ?; by subst.
Qed. Qed.
Lemma ufrac_auth_agree p a b : (U{p} a U{p} b) a b. Lemma ufrac_auth_agree p a b : (U{p} a U{p} b) a b.
......
Markdown is supported
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