fact: Definition simpl_cone (e:Psatz) : Psatz := match e with | PsatzSquare t => match t with | Pc c => if ceqb cO c then PsatzZ else PsatzC (ctimes c c) | _ => PsatzSquare t end | PsatzMulE t1 t2 => match t1 , t2 with | PsatzZ , _ => PsatzZ | _ , PsatzZ => PsatzZ | PsatzC c , PsatzC c' => PsatzC (ctimes c c') | PsatzC p1 , PsatzMulE (PsatzC p2) x => PsatzMulE (PsatzC (ctimes p1 p2)) x | PsatzC p1 , PsatzMulE x (PsatzC p2) => PsatzMulE (PsatzC (ctimes p1 p2)) x | PsatzMulE (PsatzC p2) x , PsatzC p1 => PsatzMulE (PsatzC (ctimes p1 p2)) x | PsatzMulE x (PsatzC p2) , PsatzC p1 => PsatzMulE (PsatzC (ctimes p1 p2)) x | PsatzC x , PsatzAdd y z => PsatzAdd (PsatzMulE (PsatzC x) y) (PsatzMulE (PsatzC x) z) | PsatzC c , _ => if ceqb cI c then t2 else PsatzMulE t1 t2 | _ , PsatzC c => if ceqb cI c then t1 else PsatzMulE t1 t2 | _ , _ => e end | PsatzAdd t1 t2 => match t1 , t2 with | PsatzZ , x => x | x , PsatzZ => x | x , y => PsatzAdd x y end | _ => e end.
imports: NArith Relation_Definitions Setoid Env EnvRing List Bool OrderedRing Refl