proposition: Theorem loc_of_shr_record_of_loc : forall m l, loc_of_shr_record (shr_record_of_loc m l) = l.
proof: Proof. now intros m [|[| |]]. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative