proposition: Theorem canonical_Rminus : forall (r p q : list (Term A n)) (a : Term A n) (nZa : ~ zeroP (A:=A) A0 eqA (n:=n) a), canonical A0 eqA ltM p -> canonical A0 eqA ltM q -> canonical A0 eqA ltM r -> canonical A0 eqA ltM (Rminus a nZa p q r).
proof: Proof. Proof using plusA os cs. intros r; elim r; simpl in |- *; auto. intros a l nZa p q a0 H'0 H'1 H'2 H'3. cut (canonical A0 eqA ltM l); [ idtac | apply canonical_imp_canonical with (a := a); auto ]; auto. cut (~ zeroP (A:=A) A0 eqA (n:=n) a); [ idtac | apply canonical_nzeroP with (ltM := ltM) (p := l) ]; auto. Qed.