fact: Definition m2lmul : list Z -> list Z -> list Z := fun l1 l2 => let a := nth Z0 l1 0 in let b := nth Z0 l1 1 in let c := nth Z0 l2 0 in let d := nth Z0 l2 1 in [:: Z.add (a * (c + d)) (b * c) ; Z.add (a * c) (b * d)].
imports: Coq(Extraction ZArith Lia) mathcomp(all_ssreflect all_algebra)