lemma root_root_times : ∀x,n,m,H,H1,H2.root m (root n x H H1) H2 ? =
root (m*n) x ? H1.
[cases (root_sound n x H H1);assumption
lemma root_root_times : ∀x,n,m,H,H1,H2.root m (root n x H H1) H2 ? =
root (m*n) x ? H1.
[cases (root_sound n x H H1);assumption