fact: Definition nadd := fun (sc: Z) (p1 p2: nelt) => match p1, p2 with nzero, _ => (p2, sc) | _ , nzero => (p1, sc) | (ntriple x1 y1 z1), (ntriple x2 y2 z2) => let d1 := x2 ** z1 in let d2 := x1 ** z2 in let l := d1 -- d2 in let dl := d1 ++ d2 in let m := y2 ** z1 -- y1 ** z2 in if (l ?= 0) then if (m ?= 0) then if (y1 ?= 0) then (nzero, z1 ** z2 ** sc) else let m' := 3 ** x1 ** x1 ++ A ** z1 ** z1 in let l' := 2 ** y1 ** z1 in let m'2 := m' ** m' in let l'2 := l' ** l' in let l'3 := l'2 ** l' in let x3 := m'2 ** z1 -- 2 ** x1 ** l'2 in (ntriple (l' ** x3) (l'2 ** (m' ** x1 -- y1 ** l') -- m' ** x3) (z1 ** l'3), z2 ** sc) else (nzero, m ** z1 ** z2 ** sc) else let l2 := l ** l in let l3 := l2 ** l in let m2 := m ** m in let x3 := z1 ** z2 ** m2 -- l2 ** dl in (ntriple (l ** x3) (z2 ** l2 ** (m ** x1 -- y1 ** l) -- m ** x3) (z1 ** z2 ** l3), sc) end.
imports: Ring Field_tac Ring_tac Eqdep_dec ZArith ZCAux Ppow GZnZ EGroup SMain Zmod