proposition: Lemma Rnat_div_subproof x x' (rx : refines Rnat x x') y y' (ry : refines Rnat y y') : refines (prod_R Rnat Rnat) (edivn x y) (N.div_eucl x' y').
proof: Proof. tc. Qed.
imports: ZArith Lia mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq zmodp) mathcomp(path choice fintype tuple finset ssralg ssrnum bigop ssrint) CoqEAL(hrel param refinements pos)