fact: Definition product (M N:Matrix):Matrix := let (a1,b1) := (fst (fst M), snd (fst M)) in let (c1,d1) := (fst (snd M), snd (snd M)) in let (a2,b2) := (fst (fst N), snd (fst N)) in let (c2,d2) := (fst (snd N), snd (snd N)) in ((a1 * a2 + b1 * c2, a1 * b2 + b1 * d2), (c1 * a2 + d1 * c2, c1 * b2 + d1 * d2)).
imports: Streams Streams_addenda Raxioms