+definition div2P: ∀n. \ 5a href="cic:/matita/tutorial/chapter2/Sub.ind(1,0,2)"\ 6Sub\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter2/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6\ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6\ 5span style="text-decoration: underline;"\ 6\ 5a href="cic:/matita/tutorial/chapter2/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6\ 5/span\ 6) (\ 5a href="cic:/matita/tutorial/chapter2/qr_spec.def(3)"\ 6qr_spec\ 5/a\ 6 n) ≝ λn.
+ \ 5a href="cic:/matita/tutorial/chapter2/Sub.con(0,1,2)"\ 6mk_Sub\ 5/a\ 6 ?? (\ 5a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"\ 6div2\ 5/a\ 6 n) (\ 5a href="cic:/matita/tutorial/chapter2/div2_ok.def(4)"\ 6div2_ok\ 5/a\ 6 n).
+
+(* But we can also try do directly build such an object *)
+
+definition div2Pagain : ∀n.\ 5a href="cic:/matita/tutorial/chapter2/Sub.ind(1,0,2)"\ 6Sub\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter2/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6\ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6\ 5span style="text-decoration: underline;"\ 6\ 5/span\ 6\ 5a href="cic:/matita/tutorial/chapter2/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6) (\ 5a href="cic:/matita/tutorial/chapter2/qr_spec.def(3)"\ 6qr_spec\ 5/a\ 6 n).
+#n elim n
+ [@(\ 5a href="cic:/matita/tutorial/chapter2/Sub.con(0,1,2)"\ 6mk_Sub\ 5/a\ 6 … \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"\ 6O\ 5/a\ 6,\ 5a href="cic:/matita/tutorial/chapter2/bool.con(0,2,0)"\ 6ff\ 5/a\ 6〉) normalize #q #r #H destruct //
+ |#a * #p #qrspec
+ cut (p \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6\ 5a href="cic:/matita/basics/types/fst.fix(0,2,1)"\ 6fst\ 5/a\ 6 … p, \ 5a href="cic:/matita/basics/types/snd.fix(0,2,1)"\ 6snd\ 5/a\ 6 … p〉) [//]
+ cases (\ 5a href="cic:/matita/basics/types/snd.fix(0,2,1)"\ 6snd\ 5/a\ 6 … p)
+ [#H @(\ 5a href="cic:/matita/tutorial/chapter2/Sub.con(0,1,2)"\ 6mk_Sub\ 5/a\ 6 … \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"\ 6S\ 5/a\ 6 (\ 5a href="cic:/matita/basics/types/fst.fix(0,2,1)"\ 6fst\ 5/a\ 6 … p),\ 5a href="cic:/matita/tutorial/chapter2/bool.con(0,2,0)"\ 6ff\ 5/a\ 6〉) whd #q #r #H1 destruct @\ 5a href="cic:/matita/basics/logic/eq_f.def(3)"\ 6eq_f\ 5/a\ 6 \ 5span style="text-decoration: underline;"\ 6>\ 5/span\ 6\ 5a href="cic:/matita/tutorial/chapter2/add_S.def(2)"\ 6add_S\ 5/a\ 6
+ whd in ⊢ (???%); <\ 5a href="cic:/matita/tutorial/chapter2/add_S.def(2)"\ 6add_S\ 5/a\ 6 @(qrspec … H)
+ |#H @(\ 5a href="cic:/matita/tutorial/chapter2/Sub.con(0,1,2)"\ 6mk_Sub\ 5/a\ 6 … \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6\ 5a href="cic:/matita/basics/types/fst.fix(0,2,1)"\ 6fst\ 5/a\ 6 … p,\ 5a href="cic:/matita/tutorial/chapter2/bool.con(0,1,0)"\ 6tt\ 5/a\ 6〉) whd #q #r #H1 destruct >\ 5a href="cic:/matita/tutorial/chapter2/add_S.def(2)"\ 6add_S\ 5/a\ 6 @\ 5a href="cic:/matita/basics/logic/eq_f.def(3)"\ 6eq_f\ 5/a\ 6 @(qrspec … H)
+ ]
+qed.
+
+example quotient7: \ 5a href="cic:/matita/tutorial/chapter2/witness.fix(0,2,1)"\ 6witness\ 5/a\ 6 … (\ 5a href="cic:/matita/tutorial/chapter2/div2Pagain.def(4)"\ 6div2Pagain\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"\ 6S\ 5/a\ 6(\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"\ 6S\ 5/a\ 6(\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"\ 6S\ 5/a\ 6(\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"\ 6S\ 5/a\ 6(\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"\ 6S\ 5/a\ 6(\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"\ 6S\ 5/a\ 6(\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"\ 6S\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"\ 6O\ 5/a\ 6)))))))) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"\ 6S\ 5/a\ 6(\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"\ 6S\ 5/a\ 6(\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"\ 6S\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"\ 6O\ 5/a\ 6)),\ 5a href="cic:/matita/tutorial/chapter2/bool.con(0,1,0)"\ 6tt\ 5/a\ 6〉.
+// qed.