Commit a3fd268a authored by Raphael Rieu-Helft's avatar Raphael Rieu-Helft

Partial proof of sqrt general case

parent a93167a2
This diff is collapsed.
This diff is collapsed.
......@@ -2092,5 +2092,22 @@ with wmpn_toom32_mul (r x y scratch: ptr limb) (sx sy:int32) (ghost k: int) : un
sfree scratch
end*)
meta remove_prop axiom no_borrow
meta remove_prop axiom no_borrow_ptr
meta remove_prop lemma power_ge_1
meta remove_prop axiom valuation_def
meta remove_prop axiom valuation_spec
meta remove_prop lemma valuation_mul
meta remove_prop axiom valuation_times_pow
meta remove_prop axiom valuation_lower_bound
meta remove_prop axiom valuation_monotonous
meta remove_prop lemma valuation_nondiv
meta remove_prop lemma valuation_zero_prod
meta remove_prop axiom valuation_times_nondiv
meta remove_prop lemma valuation_split
meta remove_prop lemma valuation_prod
meta remove_prop lemma valuation_mod
meta remove_prop lemma valuation_decomp
meta remove_prop lemma valuation_pow
end
\ No newline at end of file
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