proposition: Lemma plus_not_comm : {a:T1 & {b :T1 | nf a /\ nf a /\ a + b <> b + a}}.
proof: Proof. exists (finite 1); exists omega. split. simpl;repeat constructor. split. compute;repeat constructor. compute. discriminate 1. Defined.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List